# HG changeset patch
# User wenzelm
# Date 1427646748 -7200
# Node ID 62d69ffa639fe46197b47b16008c0188270b3495
# Parent  616cabc3ab519919b9527c7c6175bf609bfabcf9
more standard Sign.typ_match: sorts should be alright in result of Syntax.check_terms;

diff -r 616cabc3ab51 -r 62d69ffa639f src/Pure/Tools/rule_insts.ML
--- 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;