# HG changeset patch # User wenzelm # Date 1426880913 -3600 # Node ID a5809fbc939a983299859b0f19d79c2fbd230f02 # Parent 98b3628575805536d780db09826c6f21c43bb150 tuned; diff -r 98b362857580 -r a5809fbc939a src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Fri Mar 20 20:20:21 2015 +0100 +++ b/src/Pure/Tools/rule_insts.ML Fri Mar 20 20:48:33 2015 +0100 @@ -62,13 +62,13 @@ let val T = TVar v; val T' = f T; - in if T = T' then NONE else SOME (T, T') end; + in if T = T' then NONE else SOME (v, T') end; fun make_inst f v = let val t = Var v; val t' = f t; - in if t aconv t' then NONE else SOME (t, t') end; + in if t aconv t' then NONE else SOME (v, t') end; in @@ -94,12 +94,12 @@ val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv []; in (ts', tyenv') end; -fun read_insts ctxt in_thm mixed_insts = +fun read_insts ctxt mixed_insts thm = 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; - val (type_insts, term_insts) = partition_insts mixed_insts; + val tvars = Thm.fold_terms Term.add_tvars thm []; + val vars = Thm.fold_terms Term.add_vars thm []; (* type instantiations *) @@ -123,19 +123,19 @@ val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars; val inst_vars = map_filter (make_inst inst2) vars2; - in - (map (apply2 (Thm.ctyp_of ctxt)) inst_tvars, - map (apply2 (Thm.cterm_of ctxt)) inst_vars) - end; + in (inst_tvars, inst_vars) end; fun where_rule ctxt mixed_insts fixes thm = let val ctxt' = ctxt |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2 |> Variable.declare_thm thm; - val insts = read_insts ctxt' thm mixed_insts; + val (inst_tvars, inst_vars) = read_insts ctxt' mixed_insts thm; in - Drule.instantiate_normalize insts thm + thm + |> Drule.instantiate_normalize + (map (apply2 (Thm.ctyp_of ctxt) o apfst TVar) inst_tvars, + map (apply2 (Thm.cterm_of ctxt) o apfst Var) inst_vars) |> singleton (Proof_Context.export ctxt' ctxt) |> Rule_Cases.save thm end;