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 39557 fe5722fce758
parent 39288 f1ae2493d93f
child 42204 b3277168c1e7 
--- a/src/Pure/Proof/proof_syntax.ML	Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Mon Sep 20 16:05:25 2010 +0200
@@ -88,7 +88,7 @@
 
 fun proof_of_term thy ty =
   let
-    val thms = PureThy.all_thms_of thy;
+    val thms = Global_Theory.all_thms_of thy;
     val axms = Theory.all_axioms_of thy;
 
     fun mk_term t = (if ty then I else map_types (K dummyT))
@@ -188,7 +188,7 @@
 
 fun cterm_of_proof thy prf =
   let
-    val thm_names = map fst (PureThy.all_thms_of thy);
+    val thm_names = map fst (Global_Theory.all_thms_of thy);
     val axm_names = map fst (Theory.all_axioms_of thy);
     val thy' = thy
       |> add_proof_syntax
@@ -207,7 +207,7 @@
 
 fun read_term thy topsort =
   let
-    val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy));
+    val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy));
     val axm_names = map fst (Theory.all_axioms_of thy);
     val ctxt = thy
       |> add_proof_syntax
isabelle