untabified
authorkrauss
Tue, 07 Nov 2006 22:06:32 +0100
changeset 21237 b803f9870e97
parent 21236 890fafbcf8b0
child 21238 c46bc715bdfd
untabified
src/HOL/Tools/function_package/context_tree.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/fundef_prep.ML
src/HOL/Tools/function_package/fundef_proof.ML
src/HOL/Tools/function_package/inductive_wrap.ML
src/HOL/Tools/function_package/lexicographic_order.ML
src/HOL/Tools/function_package/mutual.ML
src/HOL/Tools/function_package/pattern_split.ML
src/HOL/Tools/function_package/sum_tools.ML
src/HOL/Tools/function_package/termination.ML
--- a/src/HOL/Tools/function_package/context_tree.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/context_tree.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -55,7 +55,7 @@
 (*** Dependency analysis for congruence rules ***)
 
 fun branch_vars t = 
-    let	
+    let 
       val t' = snd (dest_all_all t)
       val assumes = Logic.strip_imp_prems t'
       val concl = Logic.strip_imp_concl t'
@@ -64,13 +64,13 @@
 
 fun cong_deps crule =
     let
-	val branches = map branch_vars (prems_of crule)
-	val num_branches = (1 upto (length branches)) ~~ branches
+  val branches = map branch_vars (prems_of crule)
+  val num_branches = (1 upto (length branches)) ~~ branches
     in
-	IntGraph.empty
-	    |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
-	    |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
-	    (product num_branches num_branches)
+  IntGraph.empty
+      |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
+      |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
+      (product num_branches num_branches)
     end
     
 val add_congs = map (fn c => c RS eq_reflection) [cong, ext] 
@@ -80,7 +80,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 (ctx', fixes, impl) = dest_all_all_ctx ctx t
     in
       (ctx', fixes, Logic.strip_imp_prems impl, rhs_of (Logic.strip_imp_concl impl))
     end
@@ -96,7 +96,7 @@
        val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs
        val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_vars subst (Var v)))) (Term.add_vars c [])
      in
-	 (cterm_instantiate inst r, dep, branches)
+   (cterm_instantiate inst r, dep, branches)
      end
     handle Pattern.MATCH => find_cong_rule ctx fvar h rs t)
   | find_cong_rule _ _ _ [] _ = sys_error "function_package/context_tree.ML: No cong rule found!"
@@ -111,13 +111,13 @@
     | NONE => 
       if not (exists_subterm (fn Free v => v = fvar | _ => false) t) then Leaf t
       else 
-	let val (r, dep, branches) = find_cong_rule ctx fvar h congs t in
-	  Cong (t, r, dep, 
+  let val (r, dep, branches) = find_cong_rule ctx fvar h congs t in
+    Cong (t, r, dep, 
                 map (fn (ctx', fixes, assumes, st) => 
-			(fixes, map (assume o cterm_of (ProofContext.theory_of ctx)) assumes, 
+      (fixes, map (assume o cterm_of (ProofContext.theory_of ctx)) assumes, 
                          mk_tree congs fvar h ctx' st)) branches)
-	end
-		
+  end
+    
 
 fun inst_tree thy fvar f tr =
     let
@@ -142,7 +142,7 @@
 
 
 
-(* FIXME: remove *)		
+(* FIXME: remove *)   
 fun add_context_varnames (Leaf _) = I
   | add_context_varnames (Cong (_, _, _, sub)) = fold (fn (fs, _, st) => fold (insert (op =) o fst) fs o add_context_varnames st) sub
   | add_context_varnames (RCall (_,st)) = add_context_varnames st
@@ -164,30 +164,30 @@
 
 fun assume_in_ctxt thy (fixes, athms) prop =
     let
-	val global_assum = export_term (fixes, map prop_of athms) prop
+  val global_assum = export_term (fixes, map prop_of athms) prop
     in
-	(global_assum,
-	 assume (cterm_of thy global_assum) |> import_thm thy (fixes, athms))
+  (global_assum,
+   assume (cterm_of thy global_assum) |> import_thm thy (fixes, athms))
     end
 
 
 (* folds in the order of the dependencies of a graph. *)
 fun fold_deps G f x =
     let
-	fun fill_table i (T, x) =
-	    case Inttab.lookup T i of
-		SOME _ => (T, x)
-	      | NONE => 
-		let
-		    val (T', x') = fold fill_table (IntGraph.imm_succs G i) (T, x)
-		    val (v, x'') = f (the o Inttab.lookup T') i x
-		in
-		    (Inttab.update (i, v) T', x'')
-		end
+  fun fill_table i (T, x) =
+      case Inttab.lookup T i of
+    SOME _ => (T, x)
+        | NONE => 
+    let
+        val (T', x') = fold fill_table (IntGraph.imm_succs G i) (T, x)
+        val (v, x'') = f (the o Inttab.lookup T') i x
+    in
+        (Inttab.update (i, v) T', x'')
+    end
 
-	val (T, x) = fold fill_table (IntGraph.keys G) (Inttab.empty, x)
+  val (T, x) = fold fill_table (IntGraph.keys G) (Inttab.empty, x)
     in
-	(Inttab.fold (cons o snd) T [], x)
+  (Inttab.fold (cons o snd) T [], x)
     end
 
 
@@ -195,26 +195,26 @@
 
 fun traverse_tree rcOp tr x =
     let 
-	fun traverse_help ctx (Leaf _) u x = ([], x)
-	  | traverse_help ctx (RCall (t, st)) u x =
-	    rcOp ctx t u (traverse_help ctx st u x)
-	  | traverse_help ctx (Cong (t, crule, deps, branches)) u x =
-	    let
-		fun sub_step lu i x =
-		    let
-			val (fixes, assumes, subtree) = nth branches (i - 1)
-			val used = fold_rev (append o lu) (IntGraph.imm_succs deps i) u
-			val (subs, x') = traverse_help (compose ctx (fixes, assumes)) subtree used x
-			val exported_subs = map (apfst (compose (fixes, assumes))) subs
-		    in
-			(exported_subs, x')
-		    end
-	    in
-		fold_deps deps sub_step x
-			  |> apfst flatten
-	    end
+  fun traverse_help ctx (Leaf _) u x = ([], x)
+    | traverse_help ctx (RCall (t, st)) u x =
+      rcOp ctx t u (traverse_help ctx st u x)
+    | traverse_help ctx (Cong (t, crule, deps, branches)) u x =
+      let
+    fun sub_step lu i x =
+        let
+      val (fixes, assumes, subtree) = nth branches (i - 1)
+      val used = fold_rev (append o lu) (IntGraph.imm_succs deps i) u
+      val (subs, x') = traverse_help (compose ctx (fixes, assumes)) subtree used x
+      val exported_subs = map (apfst (compose (fixes, assumes))) subs
+        in
+      (exported_subs, x')
+        end
+      in
+    fold_deps deps sub_step x
+        |> apfst flatten
+      end
     in
-	snd (traverse_help ([], []) tr [] x)
+  snd (traverse_help ([], []) tr [] x)
     end
 
 
@@ -222,48 +222,47 @@
 
 fun rewrite_by_tree thy h ih x tr =
     let
-	fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x)
-	  | rewrite_help fix f_as h_as x (RCall (_ $ arg, st)) =
-	    let
-		val (inner, (lRi,ha)::x') = rewrite_help fix f_as h_as x st
-					   
-					   (* Need not use the simplifier here. Can use primitive steps! *)
-		val rew_ha = if is_refl inner then I else simplify (HOL_basic_ss addsimps [inner])
-			     
-		val h_a_eq_h_a' = combination (reflexive (cterm_of thy h)) inner
-		val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
-				     |> rew_ha
-
-		val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
-		val eq = implies_elim (implies_elim inst_ih lRi) iha
-			 
-		val h_a'_eq_f_a' = eq RS eq_reflection
-		val result = transitive h_a_eq_h_a' h_a'_eq_f_a'
-	    in
-		(result, x')
-	    end
-	  | rewrite_help fix f_as h_as x (Cong (t, crule, deps, branches)) =
-	    let
-		fun sub_step lu i x =
-		    let
-			val (fixes, assumes, st) = nth branches (i - 1)
-			val used = fold_rev (cons o lu) (IntGraph.imm_succs deps i) []
-			val used_rev = map (fn u_eq => (u_eq RS sym) RS eq_reflection) used
-			val assumes' = map (simplify (HOL_basic_ss addsimps (filter_out is_refl used_rev))) assumes
-
-			val (subeq, x') = rewrite_help (fix @ fixes) (f_as @ assumes) (h_as @ assumes') x st
-			val subeq_exp = export_thm thy (fixes, map prop_of assumes) (subeq RS meta_eq_to_obj_eq)
-		    in
-			(subeq_exp, x')
-		    end
-		    
-		val (subthms, x') = fold_deps deps sub_step x
-	    in
-		(fold_rev (curry op COMP) subthms crule, x')
-	    end
-	    
+      fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x)
+        | rewrite_help fix f_as h_as x (RCall (_ $ arg, st)) =
+          let
+            val (inner, (lRi,ha)::x') = rewrite_help fix f_as h_as x st
+                                                     
+             (* Need not use the simplifier here. Can use primitive steps! *)
+            val rew_ha = if is_refl inner then I else simplify (HOL_basic_ss addsimps [inner])
+           
+            val h_a_eq_h_a' = combination (reflexive (cterm_of thy h)) inner
+            val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
+                                 |> rew_ha
+                      
+            val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
+            val eq = implies_elim (implies_elim inst_ih lRi) iha
+                     
+            val h_a'_eq_f_a' = eq RS eq_reflection
+            val result = transitive h_a_eq_h_a' h_a'_eq_f_a'
+          in
+            (result, x')
+          end
+        | rewrite_help fix f_as h_as x (Cong (t, crule, deps, branches)) =
+          let
+            fun sub_step lu i x =
+                let
+                  val (fixes, assumes, st) = nth branches (i - 1)
+                  val used = fold_rev (cons o lu) (IntGraph.imm_succs deps i) []
+                  val used_rev = map (fn u_eq => (u_eq RS sym) RS eq_reflection) used
+                  val assumes' = map (simplify (HOL_basic_ss addsimps (filter_out is_refl used_rev))) assumes
+                                 
+                  val (subeq, x') = rewrite_help (fix @ fixes) (f_as @ assumes) (h_as @ assumes') x st
+                  val subeq_exp = export_thm thy (fixes, map prop_of assumes) (subeq RS meta_eq_to_obj_eq)
+                in
+                  (subeq_exp, x')
+                end
+                
+            val (subthms, x') = fold_deps deps sub_step x
+          in
+            (fold_rev (curry op COMP) subthms crule, x')
+          end
     in
-	rewrite_help [] [] [] x tr
+      rewrite_help [] [] [] x tr
     end
-
+    
 end
--- a/src/HOL/Tools/function_package/fundef_common.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -97,35 +97,35 @@
 
 datatype mutual_part =
   MutualPart of 
-	 {
-          fvar : string * typ,
-	  cargTs: typ list,
-	  pthA: SumTools.sum_path,
-	  pthR: SumTools.sum_path,
-	  f_def: term,
+   {
+    fvar : string * typ,
+    cargTs: typ list,
+    pthA: SumTools.sum_path,
+    pthR: SumTools.sum_path,
+    f_def: term,
 
-	  f: term option,
-          f_defthm : thm option
-	 }
-	 
+    f: term option,
+    f_defthm : thm option
+   }
+   
 
 datatype mutual_info =
   Mutual of 
-	 { 
-	  defname: string,
-          fsum_var : string * typ,
+   { 
+    defname: string,
+    fsum_var : string * typ,
 
-	  ST: typ,
-	  RST: typ,
-	  streeA: SumTools.sum_tree,
-	  streeR: SumTools.sum_tree,
+    ST: typ,
+    RST: typ,
+    streeA: SumTools.sum_tree,
+    streeR: SumTools.sum_tree,
 
-	  parts: mutual_part list,
-	  fqgars: qgar list,
-	  qglrs: ((string * typ) list * term list * term * term) list,
+    parts: mutual_part list,
+    fqgars: qgar list,
+    qglrs: ((string * typ) list * term list * term * term) list,
 
-          fsum : term option
-	 }
+    fsum : term option
+   }
 
 
 datatype prep_result =
@@ -299,12 +299,12 @@
 (* with explicit types: Needed with loose bounds *)
 fun mk_relmemT xT yT (x,y) R = 
     let 
-	val pT = HOLogic.mk_prodT (xT, yT)
-	val RT = HOLogic.mk_setT pT
+  val pT = HOLogic.mk_prodT (xT, yT)
+  val RT = HOLogic.mk_setT pT
     in
-	Const ("op :", [pT, RT] ---> boolT)
-	      $ (HOLogic.pair_const xT yT $ x $ y)
-	      $ R
+  Const ("op :", [pT, RT] ---> boolT)
+        $ (HOLogic.pair_const xT yT $ x $ y)
+        $ R
     end
 
 fun free_to_var (Free (v,T)) = Var ((v,0),T)
--- a/src/HOL/Tools/function_package/fundef_lib.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -17,18 +17,18 @@
 (* 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
+      (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))
+      (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
                          
@@ -36,10 +36,10 @@
 (* Removes all quantifiers from a term, replacing bound variables by frees. *)
 fun dest_all_all (t as (Const ("all",_) $ _)) = 
     let
-	val (v,b) = dest_all t
-	val (vs, b') = dest_all_all b
+  val (v,b) = dest_all t
+  val (vs, b') = dest_all_all b
     in
-	(v :: vs, b')
+  (v :: vs, b')
     end
   | dest_all_all t = ([],t)
 
@@ -54,7 +54,7 @@
 
       val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
     in
-	(ctx'', (n', T) :: vs, bd)
+      (ctx'', (n', T) :: vs, bd)
     end
   | dest_all_all_ctx ctx t = 
     (ctx, [], t)
--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -146,7 +146,7 @@
     in
       lthy
         |> ProofContext.note_thmss_i [(("termination",
-                                 [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
+                                        [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
         |> Proof.theorem_i PureThy.internalK NONE
                            (total_termination_afterqed name data) NONE ("", [])
                            [(("", []), [(goal, [])])]
--- a/src/HOL/Tools/function_package/fundef_prep.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -465,8 +465,7 @@
 
 fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
     let
-      fun inst_term t = 
-          subst_bound(f, abstract_over (fvar, t))
+      fun inst_term t = subst_bound(f, abstract_over (fvar, t))
     in
       (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
     end
--- a/src/HOL/Tools/function_package/fundef_proof.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_proof.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -11,7 +11,7 @@
 sig
 
     val mk_partial_rules : theory -> FundefCommon.prep_result 
-			   -> thm -> FundefCommon.fundef_result
+         -> thm -> FundefCommon.fundef_result
 end
 
 
@@ -43,128 +43,128 @@
 
 fun mk_psimp thy globals R f_iff graph_is_function clause valthm =
     let
-	val Globals {domT, z, ...} = globals
+  val Globals {domT, z, ...} = globals
 
-	val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
-	val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
-	val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
+  val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
+  val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
+  val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
     in
-	((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
-	  |> (fn it => it COMP graph_is_function)
-	  |> implies_intr z_smaller
-	  |> forall_intr (cterm_of thy z)
-	  |> (fn it => it COMP valthm)
-	  |> implies_intr lhs_acc 
-	  |> asm_simplify (HOL_basic_ss addsimps [f_iff])
-          |> fold_rev (implies_intr o cprop_of) ags
-          |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
+      ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
+        |> (fn it => it COMP graph_is_function)
+        |> implies_intr z_smaller
+        |> forall_intr (cterm_of thy z)
+        |> (fn it => it COMP valthm)
+        |> implies_intr lhs_acc 
+        |> asm_simplify (HOL_basic_ss addsimps [f_iff])
+        |> fold_rev (implies_intr o cprop_of) ags
+        |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
     end
 
 
 
 fun mk_partial_induct_rule thy globals R complete_thm clauses =
     let
-	val Globals {domT, x, z, a, P, D, ...} = globals
+  val Globals {domT, x, z, a, P, D, ...} = globals
         val acc_R = mk_acc domT R
 
-	val x_D = assume (cterm_of thy (Trueprop (D $ x)))
-	val a_D = cterm_of thy (Trueprop (D $ a))
+  val x_D = assume (cterm_of thy (Trueprop (D $ x)))
+  val a_D = cterm_of thy (Trueprop (D $ a))
 
-	val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
+  val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
 
-	val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
-	    mk_forall x
-		      (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
-						      Logic.mk_implies (Trueprop (R $ z $ x),
-									Trueprop (D $ z)))))
-		      |> cterm_of thy
+  val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
+      mk_forall x
+          (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
+                  Logic.mk_implies (Trueprop (R $ z $ x),
+                  Trueprop (D $ z)))))
+          |> cterm_of thy
 
 
-	(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
-	val ihyp = all domT $ Abs ("z", domT, 
-				   implies $ Trueprop (R $ Bound 0 $ x)
-					   $ Trueprop (P $ Bound 0))
-		       |> cterm_of thy
-
-	val aihyp = assume ihyp
+  (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
+  val ihyp = all domT $ Abs ("z", domT, 
+           implies $ Trueprop (R $ Bound 0 $ x)
+             $ Trueprop (P $ Bound 0))
+           |> cterm_of thy
 
-	fun prove_case clause =
-	    let
-		val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, rhs, case_hyp, ...}, RCs, 
-                                qglr = (oqs, _, _, _), ...} = clause
-								       
-		val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
-		val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
-		val sih = full_simplify replace_x_ss aihyp
-					
-                fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
-                    sih |> forall_elim (cterm_of thy rcarg)
-                        |> implies_elim_swp llRI
-                        |> fold_rev (implies_intr o cprop_of) CCas
-                        |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+  val aihyp = assume ihyp
 
-                val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
-			     
-		val step = Trueprop (P $ lhs)
-				    |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
-				    |> fold_rev (curry Logic.mk_implies) gs
-				    |> curry Logic.mk_implies (Trueprop (D $ lhs))
-				    |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
-				    |> cterm_of thy
-			   
-		val P_lhs = assume step
-				   |> fold forall_elim cqs
-				   |> implies_elim_swp lhs_D 
-				   |> fold_rev implies_elim_swp ags
-				   |> fold implies_elim_swp P_recs
-			    
-		val res = cterm_of thy (Trueprop (P $ x))
-				   |> Simplifier.rewrite replace_x_ss
-				   |> symmetric (* P lhs == P x *)
-				   |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
-				   |> implies_intr (cprop_of case_hyp)
-				   |> fold_rev (implies_intr o cprop_of) ags
-				   |> fold_rev forall_intr cqs
-	    in
-		(res, step)
-	    end
-
-	val (cases, steps) = split_list (map prove_case clauses)
+  fun prove_case clause =
+      let
+    val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, rhs, case_hyp, ...}, RCs, 
+                    qglr = (oqs, _, _, _), ...} = clause
+                       
+    val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
+    val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
+    val sih = full_simplify replace_x_ss aihyp
+          
+    fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
+        sih |> forall_elim (cterm_of thy rcarg)
+            |> implies_elim_swp llRI
+            |> fold_rev (implies_intr o cprop_of) CCas
+            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+        
+    val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
+                 
+    val step = Trueprop (P $ lhs)
+            |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
+            |> fold_rev (curry Logic.mk_implies) gs
+            |> curry Logic.mk_implies (Trueprop (D $ lhs))
+            |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+            |> cterm_of thy
+         
+    val P_lhs = assume step
+           |> fold forall_elim cqs
+           |> implies_elim_swp lhs_D 
+           |> fold_rev implies_elim_swp ags
+           |> fold implies_elim_swp P_recs
+          
+    val res = cterm_of thy (Trueprop (P $ x))
+           |> Simplifier.rewrite replace_x_ss
+           |> symmetric (* P lhs == P x *)
+           |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
+           |> implies_intr (cprop_of case_hyp)
+           |> fold_rev (implies_intr o cprop_of) ags
+           |> fold_rev forall_intr cqs
+      in
+    (res, step)
+      end
 
-	val istep =  complete_thm
-                       |> forall_elim_vars 0
-		       |> fold (curry op COMP) cases (*  P x  *)
-		       |> implies_intr ihyp
-		       |> implies_intr (cprop_of x_D)
-		       |> forall_intr (cterm_of thy x)
-			   
-	val subset_induct_rule = 
-	    acc_subset_induct
-		|> (curry op COMP) (assume D_subset)
-		|> (curry op COMP) (assume D_dcl)
-		|> (curry op COMP) (assume a_D)
-		|> (curry op COMP) istep
-		|> fold_rev implies_intr steps
-		|> implies_intr a_D
-		|> implies_intr D_dcl
-		|> implies_intr D_subset
+  val (cases, steps) = split_list (map prove_case clauses)
 
-	val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
+  val istep = complete_thm
+                |> forall_elim_vars 0
+                |> fold (curry op COMP) cases (*  P x  *)
+                |> implies_intr ihyp
+                |> implies_intr (cprop_of x_D)
+                |> forall_intr (cterm_of thy x)
+         
+  val subset_induct_rule = 
+      acc_subset_induct
+        |> (curry op COMP) (assume D_subset)
+        |> (curry op COMP) (assume D_dcl)
+        |> (curry op COMP) (assume a_D)
+        |> (curry op COMP) istep
+        |> fold_rev implies_intr steps
+        |> implies_intr a_D
+        |> implies_intr D_dcl
+        |> implies_intr D_subset
 
-	val simple_induct_rule =
-	    subset_induct_rule
-		|> forall_intr (cterm_of thy D)
-		|> forall_elim (cterm_of thy acc_R)
-		|> assume_tac 1 |> Seq.hd
-		|> (curry op COMP) (acc_downward
-					|> (instantiate' [SOME (ctyp_of thy domT)]
-							 (map (SOME o cterm_of thy) [R, x, z]))
-					|> forall_intr (cterm_of thy z)
-					|> forall_intr (cterm_of thy x))
-		|> forall_intr (cterm_of thy a)
-		|> forall_intr (cterm_of thy P)
+  val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
+
+  val simple_induct_rule =
+      subset_induct_rule
+        |> forall_intr (cterm_of thy D)
+        |> forall_elim (cterm_of thy acc_R)
+        |> assume_tac 1 |> Seq.hd
+        |> (curry op COMP) (acc_downward
+                              |> (instantiate' [SOME (ctyp_of thy domT)]
+                                               (map (SOME o cterm_of thy) [R, x, z]))
+                              |> forall_intr (cterm_of thy z)
+                              |> forall_intr (cterm_of thy x))
+        |> forall_intr (cterm_of thy a)
+        |> forall_intr (cterm_of thy P)
     in
-	(subset_induct_all, simple_induct_rule)
+      (subset_induct_all, simple_induct_rule)
     end
 
 
@@ -172,19 +172,19 @@
 (* Does this work with Guards??? *)
 fun mk_domain_intro thy globals R R_cases clause =
     let
-	val Globals {z, domT, ...} = globals
-	val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, 
-                        qglr = (oqs, _, _, _), ...} = clause
-	val goal = Trueprop (mk_acc domT R $ lhs)
-                     |> fold_rev (curry Logic.mk_implies) gs
-                     |> cterm_of thy
+      val Globals {z, domT, ...} = globals
+      val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, 
+                      qglr = (oqs, _, _, _), ...} = clause
+      val goal = Trueprop (mk_acc domT R $ lhs)
+                          |> fold_rev (curry Logic.mk_implies) gs
+                          |> cterm_of thy
     in
-	Goal.init goal 
-		  |> (SINGLE (resolve_tac [accI] 1)) |> the
-		  |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1))  |> the
-		  |> (SINGLE (CLASIMPSET auto_tac)) |> the
-		  |> Goal.conclude
-                  |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
+      Goal.init goal 
+      |> (SINGLE (resolve_tac [accI] 1)) |> the
+      |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1))  |> the
+      |> (SINGLE (CLASIMPSET auto_tac)) |> the
+      |> Goal.conclude
+      |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
     end
 
 
@@ -192,145 +192,145 @@
 
 fun mk_nest_term_case thy globals R' ihyp clause =
     let
-	val Globals {x, z, ...} = globals
-	val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
-                        qglr=(oqs, _, _, _), ...} = clause
-
-	val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
-
-	fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = 
-	    let
-		val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
-
-		val hyp = Trueprop (R' $ arg $ lhs)
-				    |> fold_rev (curry Logic.mk_implies o prop_of) used
-				    |> FundefCtxTree.export_term (fixes, map prop_of assumes) 
-				    |> fold_rev (curry Logic.mk_implies o prop_of) ags
-				    |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
-				    |> cterm_of thy
-
-		val thm = assume hyp
-				 |> fold forall_elim cqs
-				 |> fold implies_elim_swp ags
-				 |> FundefCtxTree.import_thm thy (fixes, assumes) (*  "(arg, lhs) : R'"  *)
-				 |> fold implies_elim_swp used
-
-		val acc = thm COMP ih_case
+      val Globals {x, z, ...} = globals
+      val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
+                      qglr=(oqs, _, _, _), ...} = clause
+          
+      val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
+                    
+      fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = 
+          let
+            val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
+                       
+            val hyp = Trueprop (R' $ arg $ lhs)
+                      |> fold_rev (curry Logic.mk_implies o prop_of) used
+                      |> FundefCtxTree.export_term (fixes, map prop_of assumes) 
+                      |> fold_rev (curry Logic.mk_implies o prop_of) ags
+                      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+                      |> cterm_of thy
+                      
+            val thm = assume hyp
+                      |> fold forall_elim cqs
+                      |> fold implies_elim_swp ags
+                      |> FundefCtxTree.import_thm thy (fixes, assumes) (*  "(arg, lhs) : R'"  *)
+                      |> fold implies_elim_swp used
+                      
+            val acc = thm COMP ih_case
+                      
+            val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
+                           
+            val arg_eq_z = (assume z_eq_arg) RS sym
+                           
+            val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
+                        |> implies_intr (cprop_of case_hyp)
+                        |> implies_intr z_eq_arg
 
-		val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
-
-		val arg_eq_z = (assume z_eq_arg) RS sym
-
-		val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
-				     |> implies_intr (cprop_of case_hyp)
-				     |> implies_intr z_eq_arg
-
-                val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
-                val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
+            val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
+            val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
+                           
+            val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
+                         |> FundefCtxTree.export_thm thy (fixes, 
+                                                          prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes))
+                         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
 
-		val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
-			       |> FundefCtxTree.export_thm thy (fixes, 
-                                                                prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes))
-                               |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
-
-		val sub' = sub @ [(([],[]), acc)]
-	    in
-		(sub', (hyp :: hyps, ethm :: thms))
-	    end
-	  | step _ _ _ _ = raise Match
+            val sub' = sub @ [(([],[]), acc)]
+          in
+            (sub', (hyp :: hyps, ethm :: thms))
+          end
+        | step _ _ _ _ = raise Match
     in
-	FundefCtxTree.traverse_tree step tree
+      FundefCtxTree.traverse_tree step tree
     end
-
-
+    
+    
 fun mk_nest_term_rule thy globals R R_cases clauses =
     let
-	val Globals { domT, x, z, ... } = globals
-        val acc_R = mk_acc domT R
-
-	val R' = Free ("R", fastype_of R)
-
-        val Rrel = Free ("R", mk_relT (domT, domT))
-        val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
-
-	val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
+      val Globals { domT, x, z, ... } = globals
+      val acc_R = mk_acc domT R
+                  
+      val R' = Free ("R", fastype_of R)
+               
+      val Rrel = Free ("R", mk_relT (domT, domT))
+      val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
+                    
+      val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
+                          
+      (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
+      val ihyp = all domT $ Abs ("z", domT, 
+                                 implies $ Trueprop (R' $ Bound 0 $ x)
+                                         $ Trueprop (acc_R $ Bound 0))
+                     |> cterm_of thy
 
-	(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
-	val ihyp = all domT $ Abs ("z", domT, 
-				   implies $ Trueprop (R' $ Bound 0 $ x)
-					   $ Trueprop (acc_R $ Bound 0))
-		       |> cterm_of thy
-
-	val ihyp_a = assume ihyp |> forall_elim_vars 0
-
-	val R_z_x = cterm_of thy (Trueprop (R $ z $ x)) 
-
-	val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
+      val ihyp_a = assume ihyp |> forall_elim_vars 0
+                   
+      val R_z_x = cterm_of thy (Trueprop (R $ z $ x)) 
+                  
+      val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
     in
-	R_cases
-            |> forall_elim (cterm_of thy z)
-            |> forall_elim (cterm_of thy x)
-            |> forall_elim (cterm_of thy (acc_R $ z))
-	    |> curry op COMP (assume R_z_x)
-	    |> fold_rev (curry op COMP) cases
-	    |> implies_intr R_z_x
-	    |> forall_intr (cterm_of thy z)
-	    |> (fn it => it COMP accI)
-	    |> implies_intr ihyp
-	    |> forall_intr (cterm_of thy x)
-	    |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
-	    |> curry op RS (assume wfR')
-	    |> fold implies_intr hyps
-	    |> implies_intr wfR'
-	    |> forall_intr (cterm_of thy R')
-            |> forall_elim (cterm_of thy (inrel_R))
-            |> curry op RS wf_in_rel
-            |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
-	    |> forall_intr (cterm_of thy Rrel)
+      R_cases
+        |> forall_elim (cterm_of thy z)
+        |> forall_elim (cterm_of thy x)
+        |> forall_elim (cterm_of thy (acc_R $ z))
+        |> curry op COMP (assume R_z_x)
+        |> fold_rev (curry op COMP) cases
+        |> implies_intr R_z_x
+        |> forall_intr (cterm_of thy z)
+        |> (fn it => it COMP accI)
+        |> implies_intr ihyp
+        |> forall_intr (cterm_of thy x)
+        |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
+        |> curry op RS (assume wfR')
+        |> fold implies_intr hyps
+        |> implies_intr wfR'
+        |> forall_intr (cterm_of thy R')
+        |> forall_elim (cterm_of thy (inrel_R))
+        |> curry op RS wf_in_rel
+        |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
+        |> forall_intr (cterm_of thy Rrel)
     end
-
+    
 
 
 
 fun mk_partial_rules thy data provedgoal =
     let
-	val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
-
-        val _ = print "Closing Derivation"
-
-	val provedgoal = Drule.close_derivation provedgoal
-
-        val _ = print "Getting gif"
-
-        val graph_is_function = (provedgoal COMP conjunctionD1)
-                                  |> forall_elim_vars 0
-
-        val _ = print "Getting cases"
-
-        val complete_thm = provedgoal COMP conjunctionD2
-
-        val _ = print "making f_iff"
-
-	val f_iff = (graph_is_function RS ex1_iff) 
-
-	val _ = Output.debug "Proving simplification rules"
-	val psimps  = map2 (mk_psimp thy globals R f_iff graph_is_function) clauses values
-
-	val _ = Output.debug "Proving partial induction rule"
-	val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy globals R complete_thm clauses
-
-	val _ = Output.debug "Proving nested termination rule"
-	val total_intro = mk_nest_term_rule thy globals R R_cases clauses
-
-	val _ = Output.debug "Proving domain introduction rules"
-	val dom_intros = map (mk_domain_intro thy globals R R_cases) clauses
+      val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
+                                                                            
+      val _ = Output.debug "Closing Derivation"
+              
+      val provedgoal = Drule.close_derivation provedgoal
+                       
+      val _ = Output.debug "Getting function theorem"
+              
+      val graph_is_function = (provedgoal COMP conjunctionD1)
+                                |> forall_elim_vars 0
+                              
+      val _ = Output.debug "Getting cases"
+              
+      val complete_thm = provedgoal COMP conjunctionD2
+                         
+      val _ = Output.debug "Making f_iff"
+              
+      val f_iff = (graph_is_function RS ex1_iff) 
+                  
+      val _ = Output.debug "Proving simplification rules"
+      val psimps  = map2 (mk_psimp thy globals R f_iff graph_is_function) clauses values
+                    
+      val _ = Output.debug "Proving partial induction rule"
+      val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy globals R complete_thm clauses
+                                             
+      val _ = Output.debug "Proving nested termination rule"
+      val total_intro = mk_nest_term_rule thy globals R R_cases clauses
+                        
+      val _ = Output.debug "Proving domain introduction rules"
+      val dom_intros = map (mk_domain_intro thy globals R R_cases) clauses
     in 
-	FundefResult {f=f, G=G, R=R, completeness=complete_thm, 
-	 psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
-	 dom_intros=dom_intros}
+      FundefResult {f=f, G=G, R=R, completeness=complete_thm, 
+                    psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
+                    dom_intros=dom_intros}
     end
-
-
+    
+    
 end
 
 
--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -3,21 +3,8 @@
     Author:     Alexander Krauss, TU Muenchen
 
 
-This is a wrapper around the inductive package which corrects some of its
-slightly annoying behaviours and makes the whole business more controllable.
-
-Specifically:
-
-- Following newer Isar conventions, declaration and definition are done in one step
-
-- The specification is expected in fully quantified form. This allows the client to 
-  control the variable order. The variables will appear in the result in the same order.
-  This is especially relevant for the elimination rule, where the order usually *does* matter.
-
-
-All this will probably become obsolete in the near future, when the new "predicate" package
-is in place.
-
+A wrapper around the inductive package, restoring the quantifiers in
+the introduction and elimination rules.
 *)
 
 signature FUNDEF_INDUCTIVE_WRAP =
@@ -36,7 +23,7 @@
     let
       val thy = theory_of_thm thm
       val frees = frees_in_term ctxt t 
-                                  |> remove (op =) lfix
+                  |> remove (op =) lfix
       val vars = Term.add_vars (prop_of thm) [] |> rev
                  
       val varmap = frees ~~ vars
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -7,8 +7,8 @@
 
 signature LEXICOGRAPHIC_ORDER =
 sig
-    val lexicographic_order : Method.method
-    val setup: theory -> theory
+  val lexicographic_order : Method.method
+  val setup: theory -> theory
 end
 
 structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
@@ -19,222 +19,222 @@
 val wf_measures = thm "wf_measures"
 val measures_less = thm "measures_less"
 val measures_lesseq = thm "measures_lesseq"
-
+                      
 fun del_index (n, []) = []
   | del_index (n, x :: xs) =
-      if n>0 then x :: del_index (n - 1, xs) else xs 
+    if n>0 then x :: del_index (n - 1, xs) else xs 
 
 fun transpose ([]::_) = []
   | transpose xss = map hd xss :: transpose (map tl xss)
 
 fun mk_sum_case (f1, f2) =
     case (fastype_of f1, fastype_of f2) of
-	(Type("fun", [A, B]), Type("fun", [C, D])) =>
-	if (B = D) then
-            Const("Datatype.sum.sum_case", (A --> B) --> (C --> D) --> Type("+", [A,C]) --> B) $ f1 $ f2
-	else raise TERM ("mk_sum_case: range type mismatch", [f1, f2]) 
-      | _ => raise TERM ("mk_sum_case", [f1, f2])
-
+      (Type("fun", [A, B]), Type("fun", [C, D])) =>
+      if (B = D) then
+        Const("Datatype.sum.sum_case", (A --> B) --> (C --> D) --> Type("+", [A,C]) --> B) $ f1 $ f2
+      else raise TERM ("mk_sum_case: range type mismatch", [f1, f2]) 
+    | _ => raise TERM ("mk_sum_case", [f1, f2])
+                 
 fun dest_wf (Const ("Wellfounded_Recursion.wf", _) $ t) = t
   | dest_wf t = raise TERM ("dest_wf", [t])
-
+                      
 datatype cell = Less of thm | LessEq of thm | None of thm | False of thm;
-
+         
 fun is_Less cell = case cell of (Less _) => true | _ => false  
-
+                                                        
 fun is_LessEq cell = case cell of (LessEq _) => true | _ => false
-
+                                                            
 fun thm_of_cell cell =
     case cell of 
-	Less thm => thm
-      | LessEq thm => thm
-      | False thm => thm
-      | None thm => thm
-			   
+      Less thm => thm
+    | LessEq thm => thm
+    | False thm => thm
+    | None thm => thm
+                  
 fun mk_base_fun_bodys (t : term) (tt : typ) =
     case tt of
-	Type("*", [ft, st]) => (mk_base_fun_bodys (Const("fst", tt --> ft) $ t) ft) @ (mk_base_fun_bodys (Const("snd", tt --> st) $ t) st)      
-      | _ => [(t, tt)]
-	     
+      Type("*", [ft, st]) => (mk_base_fun_bodys (Const("fst", tt --> ft) $ t) ft) @ (mk_base_fun_bodys (Const("snd", tt --> st) $ t) st)      
+    | _ => [(t, tt)]
+           
 fun mk_base_fun_header fulltyp (t, typ) =
     if typ = HOLogic.natT then
-	Abs ("x", fulltyp, t)
+      Abs ("x", fulltyp, t)
     else Abs ("x", fulltyp, Const("Nat.size", typ --> HOLogic.natT) $ t)
-	 	 
+         
 fun mk_base_funs (tt: typ) = 
     mk_base_fun_bodys (Bound 0) tt |>
-		      map (mk_base_fun_header tt)
-		   
+                      map (mk_base_fun_header tt)
+    
 fun mk_ext_base_funs (tt : typ) =
     case tt of
-	Type("+", [ft, st]) =>
-	product (mk_ext_base_funs ft) (mk_ext_base_funs st)
-        |> map mk_sum_case
-      | _ => mk_base_funs tt
-
+      Type("+", [ft, st]) =>
+      product (mk_ext_base_funs ft) (mk_ext_base_funs st)
+              |> map mk_sum_case
+    | _ => mk_base_funs tt
+           
 fun dest_term (t : term) =
     let
-	val (vars, prop) = (FundefLib.dest_all_all t)
-	val prems = Logic.strip_imp_prems prop
-	val (tuple, rel) = Logic.strip_imp_concl prop
-                           |> HOLogic.dest_Trueprop 
-                           |> HOLogic.dest_mem
-	val (lhs, rhs) = HOLogic.dest_prod tuple
+      val (vars, prop) = (FundefLib.dest_all_all t)
+      val prems = Logic.strip_imp_prems prop
+      val (tuple, rel) = Logic.strip_imp_concl prop
+                         |> HOLogic.dest_Trueprop 
+                         |> HOLogic.dest_mem
+      val (lhs, rhs) = HOLogic.dest_prod tuple
     in
-	(vars, prems, lhs, rhs, rel)
+      (vars, prems, lhs, rhs, rel)
     end
-
+    
 fun mk_goal (vars, prems, lhs, rhs) rel =
     let 
-	val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
-    in	
-	Logic.list_implies (prems, concl) |>
-	fold_rev FundefLib.mk_forall vars
+      val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
+    in  
+      Logic.list_implies (prems, concl) |>
+                         fold_rev FundefLib.mk_forall vars
     end
-
+    
 fun prove (thy: theory) (t: term) =
     cterm_of thy t |> Goal.init 
     |> SINGLE (CLASIMPSET auto_tac) |> the
-
+    
 fun mk_cell (thy : theory) (vars, prems) (lhs, rhs) = 
-    let	
-	val goals = mk_goal (vars, prems, lhs, rhs) 
-	val less_thm = goals "Orderings.less" |> prove thy
+    let 
+      val goals = mk_goal (vars, prems, lhs, rhs) 
+      val less_thm = goals "Orderings.less" |> prove thy
     in
-	if Thm.no_prems less_thm then
-	    Less (Goal.finish less_thm)
-	else
-	    let
-		val lesseq_thm = goals "Orderings.less_eq" |> prove thy
-	    in
-		if Thm.no_prems lesseq_thm then
-		    LessEq (Goal.finish lesseq_thm)
-		else 
-		    if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm
-		    else None lesseq_thm
-	    end
+      if Thm.no_prems less_thm then
+        Less (Goal.finish less_thm)
+      else
+        let
+          val lesseq_thm = goals "Orderings.less_eq" |> prove thy
+        in
+          if Thm.no_prems lesseq_thm then
+            LessEq (Goal.finish lesseq_thm)
+          else 
+            if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm
+            else None lesseq_thm
+        end
     end
-
+    
 fun mk_row (thy: theory) base_funs (t : term) =
     let
-	val (vars, prems, lhs, rhs, _) = dest_term t
-	val lhs_list = map (fn x => x $ lhs) base_funs
-	val rhs_list = map (fn x => x $ rhs) base_funs
+      val (vars, prems, lhs, rhs, _) = dest_term t
+      val lhs_list = map (fn x => x $ lhs) base_funs
+      val rhs_list = map (fn x => x $ rhs) base_funs
     in
-	map (mk_cell thy (vars, prems)) (lhs_list ~~ rhs_list)
+      map (mk_cell thy (vars, prems)) (lhs_list ~~ rhs_list)
     end
-
+      
 (* simple depth-first search algorithm for the table *)
 fun search_table table =
     case table of
-	[] => SOME []
-      | _ =>
-	let
-	    val check_col = forall (fn c => is_Less c orelse is_LessEq c)
-            val col = find_index (check_col) (transpose table)
-	in case col of
-	       ~1 => NONE 
-             | _ =>
-               let
-		   val order_opt = table |> filter_out (fn x => is_Less (nth x col)) |> map (curry del_index col) |> search_table
-		   val transform_order = (fn col => map (fn x => if x>=col then x+1 else x))
-               in case order_opt of
-		      NONE => NONE
-		    | SOME order =>SOME (col::(transform_order col order))
-	       end
-	end
-
+      [] => SOME []
+    | _ =>
+      let
+        val check_col = forall (fn c => is_Less c orelse is_LessEq c)
+        val col = find_index (check_col) (transpose table)
+      in case col of
+           ~1 => NONE 
+         | _ =>
+           let
+             val order_opt = table |> filter_out (fn x => is_Less (nth x col)) |> map (curry del_index col) |> search_table
+             val transform_order = (fn col => map (fn x => if x>=col then x+1 else x))
+           in case order_opt of
+                NONE => NONE
+              | SOME order =>SOME (col::(transform_order col order))
+           end
+      end
+      
 fun prove_row row (st : thm) =
     case row of
-        [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (row is empty)" 
-      | cell::tail =>
-	case cell of
-	    Less less_thm =>
-	    let
-		val next_thm = st |> SINGLE (rtac measures_less 1) |> the
-	    in
-		implies_elim next_thm less_thm
-	    end
-	  | LessEq lesseq_thm =>
-	    let
-		val next_thm = st |> SINGLE (rtac measures_lesseq 1) |> the
-	    in
-		implies_elim next_thm lesseq_thm |>
-                prove_row tail
-	    end
-          | _ => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (Only expecting Less or LessEq)"
-
+      [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (row is empty)" 
+    | cell::tail =>
+      case cell of
+        Less less_thm =>
+        let
+          val next_thm = st |> SINGLE (rtac measures_less 1) |> the
+        in
+          implies_elim next_thm less_thm
+        end
+      | LessEq lesseq_thm =>
+        let
+          val next_thm = st |> SINGLE (rtac measures_lesseq 1) |> the
+        in
+          implies_elim next_thm lesseq_thm 
+          |> prove_row tail
+        end
+      | _ => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (Only expecting Less or LessEq)"
+             
 fun pr_unprovable_subgoals table =
     filter (fn x => not (is_Less x) andalso not (is_LessEq x)) (flat table)
-	   |> map ((fn th => Pretty.string_of (Pretty.chunks (Display.pretty_goals (Thm.nprems_of th) th))) o thm_of_cell)
-
+    |> map ((fn th => Pretty.string_of (Pretty.chunks (Display.pretty_goals (Thm.nprems_of th) th))) o thm_of_cell)
+    
 fun pr_goal thy t i = 
     let
-	val (_, prems, lhs, rhs, _) = dest_term t 
-	val prterm = string_of_cterm o (cterm_of thy)
+      val (_, prems, lhs, rhs, _) = dest_term t 
+      val prterm = string_of_cterm o (cterm_of thy)
     in
-	(* also show prems? *)
+      (* also show prems? *)
         i ^ ") " ^ (prterm lhs) ^ " '<' " ^ (prterm rhs) 
     end
-
+    
 fun pr_fun thy t i =
     (string_of_int i) ^ ") " ^ (string_of_cterm (cterm_of thy t))
-
+    
 fun pr_cell cell = case cell of Less _ => " <  " 
-				| LessEq _ => " <= " 
-				| None _ => " N  "
-				| False _ => " F  "
-       
+                              | LessEq _ => " <= " 
+                              | None _ => " N  "
+                              | False _ => " F  "
+                                             
 (* fun pr_err: prints the table if tactic failed *)
 fun pr_err table thy tl base_funs =  
     let 
-	val gc = map (fn i => chr (i + 96)) (1 upto (length table))
-	val mc = 1 upto (length base_funs)
-	val tstr = ("   " ^ (concat (map (fn i => " " ^ (string_of_int i) ^ "  ") mc))) ::
-		   (map2 (fn r => fn i => i ^ ": " ^ (concat (map pr_cell r))) table gc)
-	val gstr = ("Goals:"::(map2 (pr_goal thy) tl gc))
-	val mstr = ("Measures:"::(map2 (pr_fun thy) base_funs mc))   
-	val ustr = ("Unfinished subgoals:"::(pr_unprovable_subgoals table))
+      val gc = map (fn i => chr (i + 96)) (1 upto (length table))
+      val mc = 1 upto (length base_funs)
+      val tstr = ("   " ^ (concat (map (fn i => " " ^ (string_of_int i) ^ "  ") mc))) ::
+                 (map2 (fn r => fn i => i ^ ": " ^ (concat (map pr_cell r))) table gc)
+      val gstr = ("Goals:"::(map2 (pr_goal thy) tl gc))
+      val mstr = ("Measures:"::(map2 (pr_fun thy) base_funs mc))   
+      val ustr = ("Unfinished subgoals:"::(pr_unprovable_subgoals table))
     in
-	tstr @ gstr @ mstr @ ustr
+      tstr @ gstr @ mstr @ ustr
     end
-
+      
 (* the main function: create table, search table, create relation,
    and prove the subgoals *)
 fun lexicographic_order_tac (st: thm) = 
     let
-	val thy = theory_of_thm st
-        val termination_thm = ProofContext.get_thm (Variable.thm_context st) (Name "termination")
-	val next_st = SINGLE (rtac termination_thm 1) st |> the
-        val premlist = prems_of next_st
+      val thy = theory_of_thm st
+      val termination_thm = ProofContext.get_thm (Variable.thm_context st) (Name "termination")
+      val next_st = SINGLE (rtac termination_thm 1) st |> the
+      val premlist = prems_of next_st
     in
-        case premlist of 
+      case premlist of 
             [] => error "invalid number of subgoals for this tactic - expecting at least 1 subgoal" 
           | (wf::tl) => let
-		val (var, prop) = FundefLib.dest_all wf
-		val rel = HOLogic.dest_Trueprop prop |> dest_wf |> head_of
-		val crel = cterm_of thy rel
-		val base_funs = mk_ext_base_funs (fastype_of var)
-		val _ = writeln "Creating table"
-		val table = map (mk_row thy base_funs) tl
-		val _ = writeln "Searching for lexicographic order"
-		val possible_order = search_table table
-	    in
-		case possible_order of 
-		    NONE => error (cat_lines ("Could not prove it by lexicographic order:"::(pr_err table thy tl base_funs)))
-		  | SOME order  => let
-			val clean_table = map (fn x => map (nth x) order) table
-			val funs = map (nth base_funs) order
-			val list = HOLogic.mk_list (fn x => x) (fastype_of var --> HOLogic.natT) funs
-			val relterm = Abs ("x", fastype_of var, Const(measures, (fastype_of list) --> (range_type (fastype_of rel))) $ list)
-			val crelterm = cterm_of thy relterm
-			val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
-			val _ = writeln "Proving subgoals"
-		    in
-			next_st |> cterm_instantiate [(crel, crelterm)]
-				|> SINGLE (rtac wf_measures 1) |> the
-				|> fold prove_row clean_table
-				|> Seq.single
+    val (var, prop) = FundefLib.dest_all wf
+    val rel = HOLogic.dest_Trueprop prop |> dest_wf |> head_of
+    val crel = cterm_of thy rel
+    val base_funs = mk_ext_base_funs (fastype_of var)
+    val _ = writeln "Creating table"
+    val table = map (mk_row thy base_funs) tl
+    val _ = writeln "Searching for lexicographic order"
+    val possible_order = search_table table
+      in
+    case possible_order of 
+        NONE => error (cat_lines ("Could not prove it by lexicographic order:"::(pr_err table thy tl base_funs)))
+      | SOME order  => let
+      val clean_table = map (fn x => map (nth x) order) table
+      val funs = map (nth base_funs) order
+      val list = HOLogic.mk_list (fn x => x) (fastype_of var --> HOLogic.natT) funs
+      val relterm = Abs ("x", fastype_of var, Const(measures, (fastype_of list) --> (range_type (fastype_of rel))) $ list)
+      val crelterm = cterm_of thy relterm
+      val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
+      val _ = writeln "Proving subgoals"
+        in
+      next_st |> cterm_instantiate [(crel, crelterm)]
+        |> SINGLE (rtac wf_measures 1) |> the
+        |> fold prove_row clean_table
+        |> Seq.single
                     end
             end
     end
--- a/src/HOL/Tools/function_package/mutual.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/mutual.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -50,7 +50,7 @@
 fun split_def ctxt fnames geq arities =
     let
       fun input_error msg = error (cat_lines [msg, ProofContext.string_of_term ctxt geq])
-
+                            
       val (qs, imp) = open_all_all geq
 
       val gs = Logic.strip_imp_prems imp
@@ -69,7 +69,7 @@
       fun add_bvs t is = add_loose_bnos (t, 0, is)
       val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
                   |> map (fst o nth (rev qs))
-
+                
       val _ = if null rvs then ()
               else input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
                                 ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
@@ -83,17 +83,17 @@
       val k = length args
 
       val arities' = case Symtab.lookup arities fname of
-                   NONE => Symtab.update (fname, k) arities
-                 | SOME i => if (i <> k)
-                             then input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
-                             else arities
+                       NONE => Symtab.update (fname, k) arities
+                     | SOME i => if (i <> k)
+                                 then input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
+                                 else arities
     in
-        ((fname, qs, gs, args, rhs), arities')
+      ((fname, qs, gs, args, rhs), arities')
     end
-
+    
 fun get_part fname =
     the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname)
-
+                     
 (* FIXME *)
 fun mk_prod_abs e (t1, t2) =
     let
@@ -141,7 +141,7 @@
             in
                 (MutualPart {fvar=fvar,cargTs=caTs,pthA=pthA,pthR=pthR,f_def=def,f=NONE,f_defthm=NONE}, rew)
             end
-
+            
         val (parts, rews) = split_list (map4 define fs caTss pthsA pthsR)
 
         fun convert_eqs (f, qs, gs, args, rhs) =
@@ -171,10 +171,10 @@
                                                               lthy
           in
             (MutualPart {fvar=(fname, fT), cargTs=cargTs, pthA=pthA, pthR=pthR, f_def=f_def,
-                        f=SOME f, f_defthm=SOME f_defthm },
+                         f=SOME f, f_defthm=SOME f_defthm },
              lthy')
           end
-
+          
       val Mutual { defname, fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual
       val (parts', lthy') = fold_map def (parts ~~ fixes) lthy
     in
@@ -186,39 +186,39 @@
 
 fun prepare_fundef_mutual fixes eqss default lthy =
     let
-        val mutual = analyze_eqs lthy (map fst fixes) eqss
-        val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual
-
-        val (prep_result, fsum, lthy') =
-            FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy
-
-        val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
+      val mutual = analyze_eqs lthy (map fst fixes) eqss
+      val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual
+          
+      val (prep_result, fsum, lthy') =
+          FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy
+          
+      val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
     in
       ((mutual', defname, prep_result), lthy'')
     end
-
+      
 
 (* Beta-reduce both sides of a meta-equality *)
 fun beta_norm_eq thm =
     let
-        val (lhs, rhs) = dest_equals (cprop_of thm)
-        val lhs_conv = beta_conversion false lhs
-        val rhs_conv = beta_conversion false rhs
+      val (lhs, rhs) = dest_equals (cprop_of thm)
+      val lhs_conv = beta_conversion false lhs
+      val rhs_conv = beta_conversion false rhs
     in
-        transitive (symmetric lhs_conv) (transitive thm rhs_conv)
+      transitive (symmetric lhs_conv) (transitive thm rhs_conv)
     end
-
+    
 fun beta_reduce thm = Thm.equal_elim (Thm.beta_conversion true (cprop_of thm)) thm
-
-
+                      
+                      
 fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
     let
       val thy = ProofContext.theory_of ctxt
-
+                
       val oqnames = map fst pre_qs
       val (qs, ctxt') = Variable.variant_fixes oqnames ctxt
-                                           |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
-
+                        |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
+                        
       fun inst t = subst_bounds (rev qs, t)
       val gs = map inst pre_gs
       val args = map inst pre_args
@@ -240,7 +240,7 @@
 fun recover_mutual_psimp thy RST streeR all_f_defs parts (f, _, _, args, _) import (export : thm -> thm) sum_psimp_eq =
     let
       val (MutualPart {f_defthm=SOME f_def, pthR, ...}) = get_part f parts
-
+          
       val psimp = import sum_psimp_eq
       val (simp, restore_cond) = case cprems_of psimp of
                                    [] => (psimp, I)
@@ -275,46 +275,46 @@
            |> fold_rev forall_intr xs
            |> forall_elim_vars 0
     end
-
+    
 
 fun mutual_induct_rules thy induct all_f_defs (Mutual {RST, parts, streeA, ...}) =
     let
       val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => 
-                                   Free (Pname, cargTs ---> HOLogic.boolT))
+                                       Free (Pname, cargTs ---> HOLogic.boolT))
                        (mutual_induct_Pnames (length parts))
                        parts
-
-        fun mk_P (MutualPart {cargTs, ...}) P =
-            let
-                val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
-                val atup = foldr1 HOLogic.mk_prod avars
-            in
-                tupled_lambda atup (list_comb (P, avars))
-            end
-
-        val Ps = map2 mk_P parts newPs
-        val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps
-
-        val induct_inst =
-            forall_elim (cterm_of thy case_exp) induct
-                        |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
-                        |> full_simplify (HOL_basic_ss addsimps all_f_defs)
-
-        fun mk_proj rule (MutualPart {cargTs, pthA, ...}) =
-            let
-                val afs = map_index (fn (i,T) => Free ("a" ^ string_of_int i, T)) cargTs
-                val inj = SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod afs)
-            in
-                rule
-                    |> forall_elim (cterm_of thy inj)
-                    |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
-                    |> fold_rev (forall_intr o cterm_of thy) (afs @ newPs)
-            end
-
+                       
+      fun mk_P (MutualPart {cargTs, ...}) P =
+          let
+            val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
+            val atup = foldr1 HOLogic.mk_prod avars
+          in
+            tupled_lambda atup (list_comb (P, avars))
+          end
+          
+      val Ps = map2 mk_P parts newPs
+      val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps
+                     
+      val induct_inst =
+          forall_elim (cterm_of thy case_exp) induct
+                      |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
+                      |> full_simplify (HOL_basic_ss addsimps all_f_defs)
+          
+      fun mk_proj rule (MutualPart {cargTs, pthA, ...}) =
+          let
+            val afs = map_index (fn (i,T) => Free ("a" ^ string_of_int i, T)) cargTs
+            val inj = SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod afs)
+          in
+            rule
+              |> forall_elim (cterm_of thy inj)
+              |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
+              |> fold_rev (forall_intr o cterm_of thy) (afs @ newPs)
+          end
+          
     in
       map (mk_proj induct_inst) parts
     end
-
+    
 
 
 
@@ -322,44 +322,44 @@
 fun mk_partial_rules_mutual lthy (m as Mutual {RST, parts, streeR, fqgars, ...}) data prep_result =
     let
       val thy = ProofContext.theory_of lthy
-
+                                       
       (* FIXME !? *)
-      val expand = Assumption.export false lthy (LocalTheory.target_of lthy);
-      val expand_term = Drule.term_rule thy expand;
-
+      val expand = Assumption.export false lthy (LocalTheory.target_of lthy)
+      val expand_term = Drule.term_rule thy expand
+                        
       val result = FundefProof.mk_partial_rules thy data prep_result
       val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result
-
+                                                                                                               
       val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} =>
                                mk_applied_form lthy cargTs (symmetric (Thm.freezeT f_def)))
                            parts
-
+                           
       fun mk_mpsimp fqgar sum_psimp =
           in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp
-
+          
       val mpsimps = map2 mk_mpsimp fqgars psimps
-
+                    
       val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m
       val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro
     in
       FundefMResult { f=expand_term f, G=expand_term G, R=expand_term R,
-                                  psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
-                                  cases=expand completeness, termination=expand termination,
+                      psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
+                      cases=expand completeness, termination=expand termination,
                       domintros=map expand dom_intros }
     end
-
-
-
+      
+      
+      
 (* puts an object in the "right bucket" *)
 fun store_grouped P x [] = []
   | store_grouped P x ((l, xs)::bs) =
     if P (x, l) then ((l, x::xs)::bs) else ((l, xs)::store_grouped P x bs)
-
+                                           
 fun sort_by_function (Mutual {fqgars, ...}) names xs =
-      fold_rev (store_grouped (eq_str o apfst fst))  (* fill *)
-               (map name_of_fqgar fqgars ~~ xs)      (* the name-thm pairs *)
-               (map (rpair []) names)                (* in the empty buckets labeled with names *)
-
-         |> map (snd #> map snd)                     (* and remove the labels afterwards *)
-
+    fold_rev (store_grouped (eq_str o apfst fst))  (* fill *)
+             (map name_of_fqgar fqgars ~~ xs)      (* the name-thm pairs *)
+             (map (rpair []) names)                (* in the empty buckets labeled with names *)
+             
+             |> map (snd #> map snd)                     (* and remove the labels afterwards *)
+    
 end
--- a/src/HOL/Tools/function_package/pattern_split.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/pattern_split.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -12,10 +12,10 @@
 signature FUNDEF_SPLIT =
 sig
   val split_some_equations :
-    Proof.context -> (bool * term) list -> term list list
+      Proof.context -> (bool * term) list -> term list list
 
   val split_all_equations :
-    Proof.context -> term list -> term list list
+      Proof.context -> term list -> term list list
 end
 
 structure FundefSplit : FUNDEF_SPLIT =
@@ -36,16 +36,16 @@
 fun saturate ctx vs t =
     fold (fn T => fn (vs, t) => new_var ctx vs T |> apsnd (curry op $ t))
          (binder_types (fastype_of t)) (vs, t)
-
-
+         
+         
 (* This is copied from "fundef_datatype.ML" *)
 fun inst_constrs_of thy (T as Type (name, _)) =
-        map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
-            (the (DatatypePackage.get_datatype_constrs thy name))
+    map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+        (the (DatatypePackage.get_datatype_constrs thy name))
   | inst_constrs_of thy t = (print t; sys_error "inst_constrs_of")
-
-
-
+                            
+                            
+                            
 
 fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
 fun join_product (xs, ys) = map join (product xs ys)
@@ -91,12 +91,12 @@
 fun pattern_subtract ctx eq2 eq1 =
     let
       val thy = ProofContext.theory_of ctx
-      
+                
       val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1
       val (_,  _ $ (_ $ lhs2 $ _)) = dest_all_all eq2
-
+                                     
       val substs = pattern_subtract_subst ctx vs lhs1 lhs2
-
+                   
       fun instantiate (vs', sigma) =
           let
             val t = Pattern.rewrite_term thy sigma [] feq1
@@ -106,7 +106,7 @@
     in
       map instantiate substs
     end
-
+      
 
 (* ps - p' *)
 fun pattern_subtract_from_many ctx p'=
@@ -128,7 +128,7 @@
     in
       split_aux [] eqns
     end
-
+    
 fun split_all_equations ctx =
     split_some_equations ctx o map (pair true)
 
--- a/src/HOL/Tools/function_package/sum_tools.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/sum_tools.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -46,30 +46,30 @@
   | Branch of (typ * (typ * sum_tree) * (typ * sum_tree))
 
 type sum_path = bool list (* true: left, false: right *)
-
+                
 fun sum_type_of (Leaf T) = T
   | sum_type_of (Branch (ST,(LT,_),(RT,_))) = ST
-
-
+                                              
+                                              
 fun mk_tree Ts =
     let 
-	fun mk_tree' 1 [T] = (T, Leaf T, [[]])
-	  | mk_tree' n Ts =
-	    let 
-		val n2 = n div 2
-		val (lTs, rTs) = chop n2 Ts
-		val (TL, ltree, lpaths) = mk_tree' n2 lTs
-		val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs
-		val T = mk_sumT TL TR
-		val pths = map (cons true) lpaths @ map (cons false) rpaths 
-	    in
-		(T, Branch (T, (TL, ltree), (TR, rtree)), pths)
-	    end
+      fun mk_tree' 1 [T] = (T, Leaf T, [[]])
+        | mk_tree' n Ts =
+          let 
+            val n2 = n div 2
+            val (lTs, rTs) = chop n2 Ts
+            val (TL, ltree, lpaths) = mk_tree' n2 lTs
+            val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs
+            val T = mk_sumT TL TR
+            val pths = map (cons true) lpaths @ map (cons false) rpaths 
+          in
+            (T, Branch (T, (TL, ltree), (TR, rtree)), pths)
+          end
     in
-	mk_tree' (length Ts) Ts
+      mk_tree' (length Ts) Ts
     end
-
-
+    
+    
 fun mk_tree_distinct Ts =
     let
       fun insert_once T Ts =
@@ -78,9 +78,9 @@
           in
             if i = ~1 then (length Ts, Ts @ [T]) else (i, Ts)
           end
-
+          
       val (idxs, dist_Ts) = fold_map insert_once Ts []
-
+                            
       val (ST, tree, pths) = mk_tree dist_Ts
     in
       (ST, tree, map (nth pths) idxs)
@@ -104,19 +104,19 @@
 
 fun mk_sumcases tree T ts =
     let
-	fun mk_sumcases' (Leaf _) (t::ts) = (t,ts)
-	  | mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts =
-	    let
-		val (lcase, ts') = mk_sumcases' ltr ts
-		val (rcase, ts'') = mk_sumcases' rtr ts'
-	    in
-		(mk_sumcase LT RT T lcase rcase, ts'')
-	    end
-	  | mk_sumcases' _ [] = sys_error "mk_sumcases"
+      fun mk_sumcases' (Leaf _) (t::ts) = (t,ts)
+        | mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts =
+          let
+            val (lcase, ts') = mk_sumcases' ltr ts
+            val (rcase, ts'') = mk_sumcases' rtr ts'
+          in
+            (mk_sumcase LT RT T lcase rcase, ts'')
+          end
+        | mk_sumcases' _ [] = sys_error "mk_sumcases"
     in
-	fst (mk_sumcases' tree ts)
+      fst (mk_sumcases' tree ts)
     end
-
+    
 end
 
 
--- a/src/HOL/Tools/function_package/termination.ML	Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/termination.ML	Tue Nov 07 22:06:32 2006 +0100
@@ -9,8 +9,8 @@
 
 signature FUNDEF_TERMINATION =
 sig
-    val mk_total_termination_goal : FundefCommon.result_with_names -> term
-    val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
+  val mk_total_termination_goal : FundefCommon.result_with_names -> term
+  val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
 end
 
 structure FundefTermination : FUNDEF_TERMINATION =
@@ -20,41 +20,40 @@
 open FundefLib
 open FundefCommon
 open FundefAbbrev
-
+     
 fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _) =
     let
-	val domT = domain_type (fastype_of f)
-	val x = Free ("x", domT)
+      val domT = domain_type (fastype_of f)
+      val x = Free ("x", domT)
     in
       mk_forall x (Trueprop (mk_acc domT R $ x))
     end
-
+    
 fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =
     let
-	val domT = domain_type (fastype_of f)
-	val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
-	val DT = type_of D
-	val idomT = HOLogic.dest_setT DT
-
-	val x = Free ("x", idomT)
-	val z = Free ("z", idomT)
-	val Rname = fst (dest_Const R)
-	val iRT = mk_relT (idomT, idomT)
-	val iR = Const (Rname, iRT)
-		
+      val domT = domain_type (fastype_of f)
+      val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
+      val DT = type_of D
+      val idomT = HOLogic.dest_setT DT
+                  
+      val x = Free ("x", idomT)
+      val z = Free ("z", idomT)
+      val Rname = fst (dest_Const R)
+      val iRT = mk_relT (idomT, idomT)
+      val iR = Const (Rname, iRT)
+               
+      val subs = HOLogic.mk_Trueprop 
+                   (Const ("Orderings.less_eq", DT --> DT --> boolT) $ D $
+                          (Const (acc_const_name, iRT --> DT) $ iR))
+                   |> Type.freeze
 
-	val subs = HOLogic.mk_Trueprop 
-			 (Const ("Orderings.less_eq", DT --> DT --> boolT) $ D $
-				(Const (acc_const_name, iRT --> DT) $ iR))
-			 |> Type.freeze
-
-	val dcl = mk_forall x
-			    (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)),
-							    Logic.mk_implies (mk_relmem (z, x) iR,
-									      Trueprop (mk_mem (z, D))))))
-			    |> Type.freeze
+      val dcl = mk_forall x
+                (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)),
+                                                Logic.mk_implies (mk_relmem (z, x) iR,
+                                                                  Trueprop (mk_mem (z, D))))))
+                |> Type.freeze
     in
-	(subs, dcl)
+      (subs, dcl)
     end
 
 end