--- a/src/Tools/induct.ML Wed Oct 12 21:39:33 2011 +0200
+++ b/src/Tools/induct.ML Wed Oct 12 22:21:38 2011 +0200
@@ -56,7 +56,7 @@
val predN: string
val setN: string
(*proof methods*)
- val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
+ val arbitrary_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
val add_defs: (binding option * (term * bool)) option list -> Proof.context ->
(term option list * thm list) * Proof.context
val atomize_term: theory -> term -> term
@@ -637,7 +637,7 @@
| special_rename_params _ _ ths = ths;
-(* fix_tac *)
+(* arbitrary_tac *)
local
@@ -685,8 +685,8 @@
in
-fun fix_tac _ _ [] = K all_tac
- | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
+fun arbitrary_tac _ _ [] = K all_tac
+ | arbitrary_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
(EVERY' (map (meta_spec_tac ctxt n) xs) THEN'
(miniscope_tac (goal_params n goal) ctxt)) i);
@@ -784,9 +784,9 @@
Method.insert_tac (more_facts @ adefs) THEN'
(if simp then
rotate_tac k (length adefs) THEN'
- fix_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
+ arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
else
- fix_tac defs_ctxt k xs)
+ arbitrary_tac defs_ctxt k xs)
end)
THEN' inner_atomize_tac) j))
THEN' atomize_tac) i st |> Seq.maps (fn st' =>