more standard Sign.typ_match: sorts should be alright in result of Syntax.check_terms;

--- a/src/Pure/Tools/rule_insts.ML	Sun Mar 29 18:18:52 2015 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Sun Mar 29 18:32:28 2015 +0200
@@ -92,7 +92,7 @@
       |> Syntax.check_terms ctxt'
       |> Variable.polymorphic ctxt';
     val Ts' = map Term.fastype_of ts';
-    val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
+    val tyenv = fold (Sign.typ_match (Proof_Context.theory_of ctxt)) (Ts ~~ Ts') Vartab.empty;
     val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv [];
   in ((ts', tyenv'), ctxt') end;