Fr is also reserved.

manual/src/016_syntax_description.md

@@ -220,7 +220,7 @@ the function definition.
 Facts do not have to be defined up-front. This will probably change once we
 implement user-defined sorts. Facts prefixed with `!` are persistent facts.
 All other facts are linear. There are six reserved fact symbols: In, Out, KU,
-KD, and K. KU and KD facts are used for construction and deconstruction
+KD, Fr, and K. KU and KD facts are used for construction and deconstruction
 rules. KU-facts also log the messages deduced by construction rules. Note that
 KU-facts have arity 2. Their first argument is used to track the
 exponentiation tags. See the `loops/Crypto_API_Simple.spthy` example for more