src/Pure/ML/ml_antiquote.ML
changeset 40241 56fad09655a5
parent 40110 93e7935d4cb5
child 41376 08240feb69c7
--- a/src/Pure/ML/ml_antiquote.ML	Thu Oct 28 22:59:33 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Thu Oct 28 23:19:52 2010 +0200
@@ -71,12 +71,6 @@
     "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 (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 ()");
 
 val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));