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/Pure/Proof/proof_syntax.ML
changeset 17019 f68598628d08
parent 16866 cde0b6864924
child 17078 db9d24c8b439 
--- a/src/Pure/Proof/proof_syntax.ML	Wed Aug 03 16:25:22 2005 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Wed Aug 03 16:26:16 2005 +0200
@@ -91,7 +91,7 @@
 
 fun disambiguate_names thy prf =
   let
-    val thms = thms_of_proof Symtab.empty prf;
+    val thms = thms_of_proof prf Symtab.empty;
     val thms' = map (apsnd Thm.full_prop_of) (PureThy.all_thms_of thy);
 
     val tab = Symtab.foldl (fn (tab, (key, ps)) =>
@@ -246,8 +246,8 @@
 
 fun pretty_proof thy prf =
   let
-    val thm_names = map fst (Symtab.dest (thms_of_proof Symtab.empty prf)) \ "";
-    val axm_names = map fst (Symtab.dest (axms_of_proof Symtab.empty prf));
+    val thm_names = map fst (Symtab.dest (thms_of_proof prf Symtab.empty)) \ "";
+    val axm_names = map fst (Symtab.dest (axms_of_proof prf Symtab.empty));
     val thy' = thy |>
       add_proof_syntax |>
       add_proof_atom_consts
isabelle