# HG changeset patch # User wenzelm # Date 1426879221 -3600 # Node ID 98b3628575805536d780db09826c6f21c43bb150 # Parent 745f5e43cf928bb39f79f2857b23ceb6f64aa529 tuned; diff -r 745f5e43cf92 -r 98b362857580 src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Fri Mar 20 19:05:03 2015 +0100 +++ b/src/Pure/Tools/rule_insts.ML Fri Mar 20 20:20:21 2015 +0100 @@ -78,7 +78,7 @@ 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 "Incompatible sort for typ instantiation of " (xi, pos) + else error_var "Bad sort for instantiation of type variable: " (xi, pos) end; fun read_termTs ctxt ss Ts = @@ -94,8 +94,11 @@ val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv []; in (ts', tyenv') end; -fun read_insts ctxt (tvars, vars) mixed_insts = +fun read_insts ctxt in_thm mixed_insts = let + val tvars = Thm.fold_terms Term.add_tvars in_thm []; + val vars = Thm.fold_terms Term.add_vars in_thm []; + val (type_insts, term_insts) = partition_insts mixed_insts; @@ -130,9 +133,7 @@ val ctxt' = ctxt |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2 |> Variable.declare_thm thm; - val tvars = Thm.fold_terms Term.add_tvars thm []; - val vars = Thm.fold_terms Term.add_vars thm []; - val insts = read_insts ctxt' (tvars, vars) mixed_insts; + val insts = read_insts ctxt' thm mixed_insts; in Drule.instantiate_normalize insts thm |> singleton (Proof_Context.export ctxt' ctxt)