# HG changeset patch # User wenzelm # Date 1426848514 -3600 # Node ID 558acf0426f1fd367b34055f0e7773fffd7eec66 # Parent a996f037c09dcbc62393bb896a24e2eaaa69a1dd tuned signature; diff -r a996f037c09d -r 558acf0426f1 src/HOL/Bali/AxExample.thy --- a/src/HOL/Bali/AxExample.thy Fri Mar 20 11:23:32 2015 +0100 +++ b/src/HOL/Bali/AxExample.thy Fri Mar 20 11:48:34 2015 +0100 @@ -43,7 +43,7 @@ ML {* fun inst1_tac ctxt s t xs st = (case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of - SOME i => Rule_Insts.instantiate_tac ctxt [(((s, i), Position.none), t)] xs st + SOME i => PRIMITIVE (Rule_Insts.read_instantiate ctxt [(((s, i), Position.none), t)] xs) st | NONE => Seq.empty); fun ax_tac ctxt = diff -r a996f037c09d -r 558acf0426f1 src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Fri Mar 20 11:23:32 2015 +0100 +++ b/src/Pure/Tools/rule_insts.ML Fri Mar 20 11:48:34 2015 +0100 @@ -30,8 +30,6 @@ (binding * string option * mixfix) list -> thm -> thm val read_instantiate: Proof.context -> ((indexname * Position.T) * string) list -> string list -> thm -> thm - val instantiate_tac: Proof.context -> - ((indexname * Position.T) * string) list -> string list -> tactic val make_elim_preserve: Proof.context -> thm -> thm val method: (Proof.context -> ((indexname * Position.T) * string) list -> thm -> int -> tactic) -> @@ -158,15 +156,9 @@ end; - -(* instantiation of rule or goal state *) - fun read_instantiate ctxt insts xs = where_rule ctxt insts (map (fn x => (Binding.name x, NONE, NoSyn)) xs); -fun instantiate_tac ctxt insts fixes = - PRIMITIVE (read_instantiate ctxt insts fixes); - (** attributes **)