tuned signature;
authorwenzelm
Wed Oct 12 22:21:38 2011 +0200 (2011-10-12 ago)
changeset 4513209de0d0de645
parent 45131 d7e4a7ab1061
child 45133 2214ba5bdfff
tuned signature;
src/HOL/Nominal/nominal_induct.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Wed Oct 12 21:39:33 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Wed Oct 12 22:21:38 2011 +0200
     1.3 @@ -114,10 +114,9 @@
     1.4                Method.insert_tac (more_facts @ adefs) THEN'
     1.5                  (if simp then
     1.6                     Induct.rotate_tac k (length adefs) THEN'
     1.7 -                   Induct.fix_tac defs_ctxt k
     1.8 -                     (List.partition (member op = frees) xs |> op @)
     1.9 +                   Induct.arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
    1.10                   else
    1.11 -                   Induct.fix_tac defs_ctxt k xs)
    1.12 +                   Induct.arbitrary_tac defs_ctxt k xs)
    1.13              end)
    1.14            THEN' Induct.inner_atomize_tac) j))
    1.15          THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>
     2.1 --- a/src/Tools/induct.ML	Wed Oct 12 21:39:33 2011 +0200
     2.2 +++ b/src/Tools/induct.ML	Wed Oct 12 22:21:38 2011 +0200
     2.3 @@ -56,7 +56,7 @@
     2.4    val predN: string
     2.5    val setN: string
     2.6    (*proof methods*)
     2.7 -  val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
     2.8 +  val arbitrary_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
     2.9    val add_defs: (binding option * (term * bool)) option list -> Proof.context ->
    2.10      (term option list * thm list) * Proof.context
    2.11    val atomize_term: theory -> term -> term
    2.12 @@ -637,7 +637,7 @@
    2.13    | special_rename_params _ _ ths = ths;
    2.14  
    2.15  
    2.16 -(* fix_tac *)
    2.17 +(* arbitrary_tac *)
    2.18  
    2.19  local
    2.20  
    2.21 @@ -685,8 +685,8 @@
    2.22  
    2.23  in
    2.24  
    2.25 -fun fix_tac _ _ [] = K all_tac
    2.26 -  | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
    2.27 +fun arbitrary_tac _ _ [] = K all_tac
    2.28 +  | arbitrary_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
    2.29       (EVERY' (map (meta_spec_tac ctxt n) xs) THEN'
    2.30        (miniscope_tac (goal_params n goal) ctxt)) i);
    2.31  
    2.32 @@ -784,9 +784,9 @@
    2.33                Method.insert_tac (more_facts @ adefs) THEN'
    2.34                  (if simp then
    2.35                     rotate_tac k (length adefs) THEN'
    2.36 -                   fix_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
    2.37 +                   arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
    2.38                   else
    2.39 -                   fix_tac defs_ctxt k xs)
    2.40 +                   arbitrary_tac defs_ctxt k xs)
    2.41               end)
    2.42            THEN' inner_atomize_tac) j))
    2.43          THEN' atomize_tac) i st |> Seq.maps (fn st' =>