--- a/src/HOL/Tools/res_reconstruct.ML Wed Dec 19 23:06:16 2007 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML Wed Dec 19 23:10:17 2007 +0100
@@ -95,7 +95,7 @@
val annotations = $$"," |-- term -- Scan.option ($$"," |-- termlist);
-(*<cnf_annotated> ::=Ęcnf(<name>,<formula_role>,<cnf_formula><annotations>).
+(*<cnf_annotated> ::= cnf(<name>,<formula_role>,<cnf_formula><annotations>).
The <name> could be an identifier, but we assume integers.*)
val tstp_line = (Scan.this_string "cnf" -- $$"(") |--
integer --| $$"," -- Symbol.scan_id --| $$"," --