tuned;

--- a/src/Pure/Tools/rule_insts.ML	Mon Jan 27 12:10:00 2014 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Mon Jan 27 12:16:08 2014 +0100
@@ -72,13 +72,13 @@
 
 in
 
-fun read_termTs ctxt schematic ss Ts =
+fun read_termTs ctxt ss Ts =
   let
     fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
     val ts = map2 parse Ts ss;
     val ts' =
       map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
-      |> Syntax.check_terms ((schematic ? Proof_Context.set_mode Proof_Context.mode_schematic) ctxt)
+      |> Syntax.check_terms ctxt
       |> Variable.polymorphic ctxt;
     val Ts' = map Term.fastype_of ts';
     val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
@@ -112,7 +112,7 @@
 
     val (xs, ss) = split_list term_insts;
     val Ts = map (the_type vars1) xs;
-    val (ts, inferred) = read_termTs ctxt false ss Ts;
+    val (ts, inferred) = read_termTs ctxt ss Ts;
 
     val instT2 = Term.typ_subst_TVars inferred;
     val vars2 = map (apsnd instT2) vars1;
@@ -251,7 +251,8 @@
         val (xis, ss) = Library.split_list tinsts;
         val Ts = map get_typ xis;
 
-        val (ts, envT) = read_termTs ctxt' true ss Ts;
+        val (ts, envT) =
+          read_termTs (Proof_Context.set_mode Proof_Context.mode_schematic ctxt') ss Ts;
         val envT' = map (fn (ixn, T) =>
           (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
         val cenv =