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