src/Pure/ML/ml_antiquote.ML
changeset 37868 59eed00bfd8e
parent 37304 645f849eefa7
child 40110 93e7935d4cb5
--- a/src/Pure/ML/ml_antiquote.ML	Wed Jul 21 14:27:05 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Wed Jul 21 15:02:51 2010 +0200
@@ -64,12 +64,14 @@
     >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
 
 val _ = value "theory"
-  (Scan.lift Args.name >> (fn name => "Thy_Info.get_theory " ^ ML_Syntax.print_string name)
+  (Scan.lift Args.name >> (fn name =>
+    "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
   || Scan.succeed "ML_Context.the_global_context ()");
 
 val _ = value "theory_ref"
   (Scan.lift Args.name >> (fn name =>
-    "Theory.check_thy (Thy_Info.theory " ^ ML_Syntax.print_string name ^ ")")
+    "Theory.check_thy (Context.get_theory (ML_Context.the_global_context ()) " ^
+      ML_Syntax.print_string name ^ ")")
   || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
 
 val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");