--- 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 =
--- 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 **)