src/Tools/misc_legacy.ML
changeset 42361 23f352990944
parent 42284 326f57825e1a
child 44121 44adaa6db327
--- a/src/Tools/misc_legacy.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/Tools/misc_legacy.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -26,9 +26,9 @@
 
 fun simple_read_term thy T s =
   let
-    val ctxt = ProofContext.init_global thy
-      |> ProofContext.allow_dummies
-      |> ProofContext.set_mode ProofContext.mode_schematic;
+    val ctxt = Proof_Context.init_global thy
+      |> Proof_Context.allow_dummies
+      |> Proof_Context.set_mode Proof_Context.mode_schematic;
     val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
   in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;