Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_proof.ML
changeset 47927 c35238d19bb9
parent 47926 c6d5418ee770
child 47946 33afcfad3f8d 
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue May 15 13:06:15 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue May 15 13:06:15 2012 +0200
@@ -318,7 +318,7 @@
   Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term))
                 dummy_inference
 
-val waldmeister_conjecture = "conjecture_1"
+val waldmeister_conjecture_name = "conjecture_1"
 
 val tofof_fact_prefix = "fof_"
 
@@ -380,7 +380,7 @@
               (* Waldmeister isn't exactly helping. *)
               case deps of
                 File_Source (_, SOME s) =>
-                (if s = waldmeister_conjecture then
+                (if s = waldmeister_conjecture_name then
                    case find_formula_in_problem problem (mk_anot phi) of
                      (* Waldmeister hack: Get the original orientation of the
                         equation to avoid confusing Isar. *)
isabelle