# HG changeset patch
# User krauss
# Date 1292231727 -3600
# Node ID d6379876ec4ccb584547473c7ac6ba0e606dfc71
# Parent  7230a7c379dcad49e41d8a185ac9b02ccfd8ef85
eliminated dest_all_all_ctx

diff -r 7230a7c379dc -r d6379876ec4c src/HOL/Tools/Function/context_tree.ML
--- a/src/HOL/Tools/Function/context_tree.ML	Mon Dec 13 10:15:26 2010 +0100
+++ b/src/HOL/Tools/Function/context_tree.ML	Mon Dec 13 10:15:27 2010 +0100
@@ -103,7 +103,7 @@
 (* Called on the INSTANTIATED branches of the congruence rule *)
 fun mk_branch ctx t =
   let
-    val (ctx', fixes, impl) = dest_all_all_ctx ctx t
+    val ((fixes, impl), ctx') = Function_Lib.focus_term t ctx
     val (assms, concl) = Logic.strip_horn impl
   in
     (ctx', fixes, assms, rhs_of concl)
diff -r 7230a7c379dc -r d6379876ec4c src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Mon Dec 13 10:15:26 2010 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML	Mon Dec 13 10:15:27 2010 +0100
@@ -11,7 +11,6 @@
 
   val focus_term: term -> Proof.context -> ((string * typ) list * term) * Proof.context
   val dest_all_all: term -> term list * term
-  val dest_all_all_ctx: Proof.context -> term -> Proof.context * (string * typ) list * term
 
   val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
   val map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) -> 'a list -> 'b list -> 'c list ->
@@ -66,10 +65,6 @@
   | dest_all_all t = ([],t)
 
 
-fun dest_all_all_ctx ctxt t =
-  let val ((vs, b), ctxt') = focus_term t ctxt
-  in (ctxt, vs, b) end
-
 fun map4 _ [] [] [] [] = []
   | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
   | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
diff -r 7230a7c379dc -r d6379876ec4c src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Mon Dec 13 10:15:26 2010 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Mon Dec 13 10:15:27 2010 +0100
@@ -55,7 +55,7 @@
 
 fun dest_hhf ctxt t =
   let
-    val (ctxt', vars, imp) = dest_all_all_ctx ctxt t
+    val ((vars, imp), ctxt') = Function_Lib.focus_term t ctxt
   in
     (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
   end
diff -r 7230a7c379dc -r d6379876ec4c src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Mon Dec 13 10:15:26 2010 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Mon Dec 13 10:15:27 2010 +0100
@@ -165,7 +165,7 @@
         "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
 
     val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
-    val (_, _, plain_eqn) = Function_Lib.dest_all_all_ctx lthy eqn;
+    val ((_, plain_eqn), _) = Function_Lib.focus_term eqn lthy;
 
     val ((f_binding, fT), mixfix) = the_single fixes;
     val fname = Binding.name_of f_binding;