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/Thy/thy_info.ML
changeset 26425 6561665c5cb1
parent 26415 1b624d6e9163
child 26455 1757a6e049f4 
--- a/src/Pure/Thy/thy_info.ML	Thu Mar 27 14:41:09 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML	Thu Mar 27 14:41:10 2008 +0100
@@ -206,13 +206,13 @@
 val _ = ML_Context.value_antiq "theory"
   (Scan.lift Args.name
     >> (fn name => (name ^ "_thy", "ThyInfo.theory " ^ ML_Syntax.print_string name))
-  || Scan.succeed ("thy", "ML_Context.the_context ()"));
+  || Scan.succeed ("thy", "ML_Context.the_global_context ()"));
 
 val _ = ML_Context.value_antiq "theory_ref"
   (Scan.lift Args.name
     >> (fn name => (name ^ "_thy",
         "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")"))
-  || Scan.succeed ("thy", "Theory.check_thy (ML_Context.the_context ())"));
+  || Scan.succeed ("thy", "Theory.check_thy (ML_Context.the_global_context ())"));
 
 
 
@@ -603,8 +603,6 @@
     else CRITICAL (fn () => (change_thys register; perform Update name))
   end;
 
-val _ = register_theory ProtoPure.thy;
-
 
 (* finish all theories *)
isabelle