1.1 --- a/src/Pure/Isar/rule_insts.ML	Thu Nov 08 20:08:09 2007 +0100
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu Nov 08 20:08:11 2007 +0100
     1.3 @@ -117,7 +117,7 @@
     1.4  
     1.5      val (xs, strs) = split_list external_insts;
     1.6      val Ts = map (the_type vars2) xs;
     1.7 -    val (ts, inferred) = read_termTs ctxt true (* FIXME false *) strs Ts;
     1.8 +    val (ts, inferred) = read_termTs ctxt false strs Ts;
     1.9  
    1.10      val instT3 = Term.typ_subst_TVars inferred;
    1.11      val vars3 = map (apsnd instT3) vars2;