eliminated dest_all_all_ctx
authorkrauss
Mon Dec 13 10:15:27 2010 +0100 (2010-12-13)
changeset 41117d6379876ec4c
parent 41116 7230a7c379dc
child 41118 b290841cd3b0
eliminated dest_all_all_ctx
src/HOL/Tools/Function/context_tree.ML
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/partial_function.ML
     1.1 --- a/src/HOL/Tools/Function/context_tree.ML	Mon Dec 13 10:15:26 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/context_tree.ML	Mon Dec 13 10:15:27 2010 +0100
     1.3 @@ -103,7 +103,7 @@
     1.4  (* Called on the INSTANTIATED branches of the congruence rule *)
     1.5  fun mk_branch ctx t =
     1.6    let
     1.7 -    val (ctx', fixes, impl) = dest_all_all_ctx ctx t
     1.8 +    val ((fixes, impl), ctx') = Function_Lib.focus_term t ctx
     1.9      val (assms, concl) = Logic.strip_horn impl
    1.10    in
    1.11      (ctx', fixes, assms, rhs_of concl)
     2.1 --- a/src/HOL/Tools/Function/function_lib.ML	Mon Dec 13 10:15:26 2010 +0100
     2.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Mon Dec 13 10:15:27 2010 +0100
     2.3 @@ -11,7 +11,6 @@
     2.4  
     2.5    val focus_term: term -> Proof.context -> ((string * typ) list * term) * Proof.context
     2.6    val dest_all_all: term -> term list * term
     2.7 -  val dest_all_all_ctx: Proof.context -> term -> Proof.context * (string * typ) list * term
     2.8  
     2.9    val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
    2.10    val map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) -> 'a list -> 'b list -> 'c list ->
    2.11 @@ -66,10 +65,6 @@
    2.12    | dest_all_all t = ([],t)
    2.13  
    2.14  
    2.15 -fun dest_all_all_ctx ctxt t =
    2.16 -  let val ((vs, b), ctxt') = focus_term t ctxt
    2.17 -  in (ctxt, vs, b) end
    2.18 -
    2.19  fun map4 _ [] [] [] [] = []
    2.20    | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
    2.21    | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
     3.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Mon Dec 13 10:15:26 2010 +0100
     3.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Mon Dec 13 10:15:27 2010 +0100
     3.3 @@ -55,7 +55,7 @@
     3.4  
     3.5  fun dest_hhf ctxt t =
     3.6    let
     3.7 -    val (ctxt', vars, imp) = dest_all_all_ctx ctxt t
     3.8 +    val ((vars, imp), ctxt') = Function_Lib.focus_term t ctxt
     3.9    in
    3.10      (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
    3.11    end
     4.1 --- a/src/HOL/Tools/Function/partial_function.ML	Mon Dec 13 10:15:26 2010 +0100
     4.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Mon Dec 13 10:15:27 2010 +0100
     4.3 @@ -165,7 +165,7 @@
     4.4          "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
     4.5  
     4.6      val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
     4.7 -    val (_, _, plain_eqn) = Function_Lib.dest_all_all_ctx lthy eqn;
     4.8 +    val ((_, plain_eqn), _) = Function_Lib.focus_term eqn lthy;
     4.9  
    4.10      val ((f_binding, fT), mixfix) = the_single fixes;
    4.11      val fname = Binding.name_of f_binding;