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/Isar/code.ML
changeset 36610 bafd82950e24
parent 36209 566be5d48090
child 36615 88756a5a92fc 
--- a/src/Pure/Isar/code.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/code.ML	Mon May 03 14:25:56 2010 +0200
@@ -337,7 +337,7 @@
 fun cert_signature thy = Logic.varifyT_global o Type.cert_typ (build_tsig thy) o Type.no_tvars;
 
 fun read_signature thy = cert_signature thy o Type.strip_sorts
-  o Syntax.parse_typ (ProofContext.init thy);
+  o Syntax.parse_typ (ProofContext.init_global thy);
 
 fun expand_signature thy = Type.cert_typ_mode Type.mode_syntax (Sign.tsig_of thy);
 
@@ -554,7 +554,7 @@
 
 fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
 
-fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (ProofContext.init thy);
+fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (ProofContext.init_global thy);
 
 fun mk_eqn thy = error_thm (gen_assert_eqn thy false) o
   apfst (meta_rewrite thy);
@@ -941,7 +941,7 @@
 
 fun print_codesetup thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val exec = the_exec thy;
     fun pretty_equations const thms =
       (Pretty.block o Pretty.fbreaks) (
isabelle