diff -r 4bb0fc92247b -r fcb897b39fa3 src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Wed Dec 14 12:10:44 2011 +0100
+++ b/src/Tools/misc_legacy.ML	Wed Dec 14 12:18:19 2011 +0100
@@ -22,7 +22,6 @@
   val term_frees: term -> term list
   val mk_defpair: term * term -> string * term
   val get_def: theory -> xstring -> thm
-  val simple_read_term: theory -> typ -> string -> term
   val METAHYPS: (thm list -> tactic) -> int -> tactic
 end;
 
@@ -104,15 +103,6 @@
 fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
 
 
-fun simple_read_term thy T s =
-  let
-    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;
-
-
 (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
        METAHYPS (fn prems => tac prems) i