src/Pure/Tools/rule_insts.ML

     (binding * string option * mixfix) list -> thm -> thm
   val of_rule: Proof.context -> string option list * string option list ->
     (binding * string option * mixfix) list -> thm -> thm
   val read_instantiate: Proof.context ->
     ((indexname * Position.T) * string) list -> string list -> thm -> thm
+  val read_term: string -> Proof.context -> term * Proof.context
   val schematic: bool Config.T
   val goal_context: int -> thm -> Proof.context -> (string * typ) list * Proof.context
   val res_inst_tac: Proof.context ->
     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
     int -> tactic

     val T = Syntax.read_typ ctxt s;
   in
     if Sign.of_sort (Proof_Context.theory_of ctxt) (T, S) then ((xi, S), T)
     else error_var "Bad sort for instantiation of type variable: " (xi, pos)
   end;
+
+fun make_instT f v =
+  let
+    val T = TVar v;
+    val T' = f T;
+  in if T = T' then NONE else SOME (v, T') end;
+
+fun make_inst f v =
+  let
+    val t = Var v;
+    val t' = f t;
+  in if t aconv t' then NONE else SOME (v, t') end;
 
 fun read_terms ss Ts ctxt =
   let
     fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
     val (ts, ctxt') = fold_map Variable.fix_dummy_patterns (map2 parse Ts ss) ctxt;

     val Ts' = map Term.fastype_of ts';
     val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
     val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv [];
   in ((ts', tyenv'), ctxt') end;
 
-fun make_instT f v =
-  let
-    val T = TVar v;
-    val T' = f T;
-  in if T = T' then NONE else SOME (v, T') end;
-
-fun make_inst f v =
-  let
-    val t = Var v;
-    val t' = f t;
-  in if t aconv t' then NONE else SOME (v, t') end;
-
 in
+
+fun read_term s ctxt =
+  let
+    val (t, ctxt') = Variable.fix_dummy_patterns (Syntax.parse_term ctxt s) ctxt;
+    val t' = Syntax.check_term ctxt' t;
+  in (t', ctxt') end;
 
 fun read_insts thm mixed_insts ctxt =
   let
     val (type_insts, term_insts) =
       List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) mixed_insts;