# HG changeset patch
# User berghofe
# Date 1123079176 -7200
# Node ID f68598628d08730fabf0247ffbdae0503d9c393e
# Parent  1e9e0f5877f29df070ad9755e4e9efeb55851f2c
Adapted to new interface og thms_of_proof / axms_of_proof.

diff -r 1e9e0f5877f2 -r f68598628d08 src/Pure/Proof/proof_syntax.ML
--- 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