# HG changeset patch
# User krauss
# Date 1162811084 -3600
# Node ID 2aa15b663cd403d494da30910d8a64181cf08a0d
# Parent  16fb5afbf2285b2b5d47cd1bf33ae6bae1ff5875
minor cleanup

diff -r 16fb5afbf228 -r 2aa15b663cd4 src/HOL/Tools/function_package/context_tree.ML
--- a/src/HOL/Tools/function_package/context_tree.ML	Sun Nov 05 21:44:42 2006 +0100
+++ b/src/HOL/Tools/function_package/context_tree.ML	Mon Nov 06 12:04:44 2006 +0100
@@ -55,8 +55,11 @@
 (*** Dependency analysis for congruence rules ***)
 
 fun branch_vars t = 
-    let	val (assumes, term) = dest_implies_list (snd (dest_all_all t))
-    in (fold (curry add_term_vars) assumes [], term_vars term)
+    let	
+      val t' = snd (dest_all_all t)
+      val assumes = Logic.strip_imp_prems t'
+      val concl = Logic.strip_imp_concl t'
+    in (fold (curry add_term_vars) assumes [], term_vars concl)
     end
 
 fun cong_deps crule =
@@ -78,9 +81,8 @@
 fun mk_branch ctx t = 
     let
 	val (ctx', fixes, impl) = dest_all_all_ctx ctx t
-	val (assumes, term) = dest_implies_list impl
     in
-      (ctx', fixes, assumes, rhs_of term)
+      (ctx', fixes, Logic.strip_imp_prems impl, rhs_of (Logic.strip_imp_concl impl))
     end
 
 fun find_cong_rule ctx fvar h ((r,dep)::rs) t =
diff -r 16fb5afbf228 -r 2aa15b663cd4 src/HOL/Tools/function_package/fundef_lib.ML
--- a/src/HOL/Tools/function_package/fundef_lib.ML	Sun Nov 05 21:44:42 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Mon Nov 06 12:04:44 2006 +0100
@@ -12,29 +12,26 @@
 
 fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *)
 
-fun mk_forall (var as Free (v,T)) t =
-    all T $ Abs (v,T, abstract_over (var,t))
-  | mk_forall v _ = let val _ = print v in sys_error "mk_forall" end
-
+fun mk_forall v t = all (fastype_of v) $ lambda v t
 
 (* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *)
 fun tupled_lambda vars t =
     case vars of
-	(Free v) => lambda (Free v) t
-      | (Var v) => lambda (Var v) t
-      | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>  
-	(HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
-      | _ => raise Match
-
-
+	    (Free v) => lambda (Free v) t
+    | (Var v) => lambda (Var v) t
+    | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>  
+	    (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
+    | _ => raise Match
+                 
+                 
 fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
     let
-	val (n, body) = Term.dest_abs a
+	    val (n, body) = Term.dest_abs a
     in
-	(Free (n, T), body)
+	    (Free (n, T), body)
     end
   | dest_all _ = raise Match
-
+                         
 
 (* Removes all quantifiers from a term, replacing bound variables by frees. *)
 fun dest_all_all (t as (Const ("all",_) $ _)) = 
@@ -63,13 +60,6 @@
     (ctx, [], t)
 
 
-
-(* unfold *)
-fun unfold P f g b x = if (P x) then ((f x)::(unfold P f g b (g x))) else (b x)
-
-val dest_implies_list = 
-    split_last o (unfold (can Logic.dest_implies) (fst o Logic.dest_implies) (snd o Logic.dest_implies) single)
-
 fun implies_elim_swp a b = implies_elim b a
 
 fun map3 _ [] [] [] = []
diff -r 16fb5afbf228 -r 2aa15b663cd4 src/HOL/Tools/function_package/fundef_prep.ML
--- a/src/HOL/Tools/function_package/fundef_prep.ML	Sun Nov 05 21:44:42 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Mon Nov 06 12:04:44 2006 +0100
@@ -48,33 +48,31 @@
     end
 
 
-
-(* !!qs' qs. Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
-(* Takes bound form of qglrs tuples *)
-fun mk_compat_impl domT ranT fvar f ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
+fun mk_compat_proof_obligations domT ranT fvar f glrs =
     let
-      val shift = incr_boundvars (length qs')
+      fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
+          let
+            val shift = incr_boundvars (length qs')
+          in
+            (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
+                     $ Trueprop (eq_const ranT $ shift rhs $ rhs'))
+              |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
+              |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
+              |> curry abstract_over fvar
+              |> curry subst_bound f
+          end
     in
-      (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
-               $ Trueprop (eq_const ranT $ shift rhs $ rhs'))
-        |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
-        |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
-        |> curry abstract_over fvar
-        |> curry subst_bound f
+      map mk_impl (unordered_pairs glrs)
     end
 
-fun mk_compat_proof_obligations domT ranT fvar f glrs =
-    map (mk_compat_impl domT ranT fvar f) (unordered_pairs glrs)
 
-
-fun mk_completeness globals clauses qglrs =
+fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
     let
-        val Globals {x, Pbool, ...} = globals
-
-        fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = Trueprop Pbool
-                                                |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
-                                                |> fold_rev (curry Logic.mk_implies) gs
-                                                |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+        fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
+            Trueprop Pbool
+                     |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
+                     |> fold_rev (curry Logic.mk_implies) gs
+                     |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
     in
         Trueprop Pbool
                  |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
@@ -244,15 +242,6 @@
     end
 
 
-
-
-fun pr (s:string) x =
-    let val _ = print s
-    in
-      x
-    end
-
-
 fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
     let
         val Globals {h, y, x, fvar, ...} = globals