new year's resolution: reindented code in function package
authorkrauss
Sat, 02 Jan 2010 23:18:58 +0100
changeset 34232 36a2a3029fd3
parent 34231 da4d7d40f2f9
child 34233 156c42518cfc
new year's resolution: reindented code in function package
src/HOL/Tools/Function/context_tree.ML
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/function_common.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/measure_functions.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Function/pattern_split.ML
src/HOL/Tools/Function/relation.ML
src/HOL/Tools/Function/sum_tree.ML
src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/context_tree.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/context_tree.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -1,39 +1,41 @@
 (*  Title:      HOL/Tools/Function/context_tree.ML
     Author:     Alexander Krauss, TU Muenchen
 
-A package for general recursive function definitions. 
+A package for general recursive function definitions.
 Builds and traverses trees of nested contexts along a term.
 *)
 
 signature FUNCTION_CTXTREE =
 sig
-    type ctxt = (string * typ) list * thm list (* poor man's contexts: fixes + assumes *)
-    type ctx_tree
+  (* poor man's contexts: fixes + assumes *)
+  type ctxt = (string * typ) list * thm list
+  type ctx_tree
 
-    (* FIXME: This interface is a mess and needs to be cleaned up! *)
-    val get_function_congs : Proof.context -> thm list
-    val add_function_cong : thm -> Context.generic -> Context.generic
-    val map_function_congs : (thm list -> thm list) -> Context.generic -> Context.generic
+  (* FIXME: This interface is a mess and needs to be cleaned up! *)
+  val get_function_congs : Proof.context -> thm list
+  val add_function_cong : thm -> Context.generic -> Context.generic
+  val map_function_congs : (thm list -> thm list) -> Context.generic -> Context.generic
 
-    val cong_add: attribute
-    val cong_del: attribute
+  val cong_add: attribute
+  val cong_del: attribute
 
-    val mk_tree: (string * typ) -> term -> Proof.context -> term -> ctx_tree
+  val mk_tree: (string * typ) -> term -> Proof.context -> term -> ctx_tree
 
-    val inst_tree: theory -> term -> term -> ctx_tree -> ctx_tree
+  val inst_tree: theory -> term -> term -> ctx_tree -> ctx_tree
 
-    val export_term : ctxt -> term -> term
-    val export_thm : theory -> ctxt -> thm -> thm
-    val import_thm : theory -> ctxt -> thm -> thm
+  val export_term : ctxt -> term -> term
+  val export_thm : theory -> ctxt -> thm -> thm
+  val import_thm : theory -> ctxt -> thm -> thm
 
-    val traverse_tree : 
+  val traverse_tree :
    (ctxt -> term ->
    (ctxt * thm) list ->
    (ctxt * thm) list * 'b ->
    (ctxt * thm) list * 'b)
    -> ctx_tree -> 'b -> 'b
 
-    val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list -> ctx_tree -> thm * (thm * thm) list
+  val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list ->
+    ctx_tree -> thm * (thm * thm) list
 end
 
 structure Function_Ctx_Tree : FUNCTION_CTXTREE =
@@ -64,8 +66,8 @@
 
 type depgraph = int IntGraph.T
 
-datatype ctx_tree 
-  = Leaf of term
+datatype ctx_tree =
+  Leaf of term
   | Cong of (thm * depgraph * (ctxt * ctx_tree) list)
   | RCall of (term * ctx_tree)
 
@@ -76,204 +78,210 @@
 
 (*** Dependency analysis for congruence rules ***)
 
-fun branch_vars t = 
-    let 
-      val t' = snd (dest_all_all t)
-      val (assumes, concl) = Logic.strip_horn t'
-    in (fold Term.add_vars assumes [], Term.add_vars concl [])
-    end
+fun branch_vars t =
+  let
+    val t' = snd (dest_all_all t)
+    val (assumes, concl) = Logic.strip_horn t'
+  in
+    (fold Term.add_vars assumes [], Term.add_vars concl [])
+  end
 
 fun cong_deps crule =
-    let
-      val num_branches = map_index (apsnd branch_vars) (prems_of crule)
-    in
-      IntGraph.empty
-        |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
-        |> fold_product (fn (i, (c1, _)) => fn (j, (_, t2)) => 
-               if i = j orelse null (inter (op =) c1 t2)
-               then I else IntGraph.add_edge_acyclic (i,j))
-             num_branches num_branches
+  let
+    val num_branches = map_index (apsnd branch_vars) (prems_of crule)
+  in
+    IntGraph.empty
+    |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
+    |> fold_product (fn (i, (c1, _)) => fn (j, (_, t2)) =>
+         if i = j orelse null (inter (op =) c1 t2)
+         then I else IntGraph.add_edge_acyclic (i,j))
+       num_branches num_branches
     end
-    
-val default_congs = map (fn c => c RS eq_reflection) [@{thm "cong"}, @{thm "ext"}] 
 
-
+val default_congs =
+  map (fn c => c RS eq_reflection) [@{thm "cong"}, @{thm "ext"}]
 
 (* 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 (assms, concl) = Logic.strip_horn impl
-    in
-      (ctx', fixes, assms, rhs_of concl)
-    end
-    
+fun mk_branch ctx t =
+  let
+    val (ctx', fixes, impl) = dest_all_all_ctx ctx t
+    val (assms, concl) = Logic.strip_horn impl
+  in
+    (ctx', fixes, assms, rhs_of concl)
+  end
+
 fun find_cong_rule ctx fvar h ((r,dep)::rs) t =
-    (let
-       val thy = ProofContext.theory_of ctx
+  (let
+     val thy = ProofContext.theory_of ctx
 
-       val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t)
-       val (c, subs) = (concl_of r, prems_of r)
+     val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t)
+     val (c, subs) = (concl_of r, prems_of r)
 
-       val subst = Pattern.match (ProofContext.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty)
-       val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_term subst) subs
-       val inst = map (fn v =>
-        (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) (Term.add_vars c [])
-     in
-   (cterm_instantiate inst r, dep, branches)
-     end
-    handle Pattern.MATCH => find_cong_rule ctx fvar h rs t)
+     val subst = Pattern.match (ProofContext.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty)
+     val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_term subst) subs
+     val inst = map (fn v =>
+       (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) (Term.add_vars c [])
+   in
+     (cterm_instantiate inst r, dep, branches)
+   end
+   handle Pattern.MATCH => find_cong_rule ctx fvar h rs t)
   | find_cong_rule _ _ _ [] _ = sys_error "Function/context_tree.ML: No cong rule found!"
 
 
 fun mk_tree fvar h ctxt t =
-    let 
-      val congs = get_function_congs ctxt
-      val congs_deps = map (fn c => (c, cong_deps c)) (congs @ default_congs) (* FIXME: Save in theory *)
+  let
+    val congs = get_function_congs ctxt
 
-      fun matchcall (a $ b) = if a = Free fvar then SOME b else NONE
-        | matchcall _ = NONE
+    (* FIXME: Save in theory: *)
+    val congs_deps = map (fn c => (c, cong_deps c)) (congs @ default_congs)
+
+    fun matchcall (a $ b) = if a = Free fvar then SOME b else NONE
+      | matchcall _ = NONE
 
-      fun mk_tree' ctx t =
-          case matchcall t of
-            SOME arg => RCall (t, mk_tree' ctx arg)
-          | 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_deps t in
-                Cong (r, dep, 
-                      map (fn (ctx', fixes, assumes, st) => 
-                              ((fixes, map (assume o cterm_of (ProofContext.theory_of ctx)) assumes), 
-                               mk_tree' ctx' st)) branches)
-              end
-    in
-      mk_tree' ctxt t
-    end
-    
+    fun mk_tree' ctx t =
+      case matchcall t of
+        SOME arg => RCall (t, mk_tree' ctx arg)
+      | 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_deps t
+            fun subtree (ctx', fixes, assumes, st) =
+              ((fixes,
+                map (assume o cterm_of (ProofContext.theory_of ctx)) assumes),
+               mk_tree' ctx' st)
+          in
+            Cong (r, dep, map subtree branches)
+          end
+  in
+    mk_tree' ctxt t
+  end
 
 fun inst_tree thy fvar f tr =
-    let
-      val cfvar = cterm_of thy fvar
-      val cf = cterm_of thy f
-               
-      fun inst_term t = 
-          subst_bound(f, abstract_over (fvar, t))
+  let
+    val cfvar = cterm_of thy fvar
+    val cf = cterm_of thy f
 
-      val inst_thm = forall_elim cf o forall_intr cfvar 
+    fun inst_term t =
+      subst_bound(f, abstract_over (fvar, t))
+
+    val inst_thm = forall_elim cf o forall_intr cfvar
 
-      fun inst_tree_aux (Leaf t) = Leaf t
-        | inst_tree_aux (Cong (crule, deps, branches)) =
-          Cong (inst_thm crule, deps, map inst_branch branches)
-        | inst_tree_aux (RCall (t, str)) =
-          RCall (inst_term t, inst_tree_aux str)
-      and inst_branch ((fxs, assms), str) = 
-          ((fxs, map (assume o cterm_of thy o inst_term o prop_of) assms), inst_tree_aux str)
-    in
-      inst_tree_aux tr
-    end
+    fun inst_tree_aux (Leaf t) = Leaf t
+      | inst_tree_aux (Cong (crule, deps, branches)) =
+        Cong (inst_thm crule, deps, map inst_branch branches)
+      | inst_tree_aux (RCall (t, str)) =
+        RCall (inst_term t, inst_tree_aux str)
+    and inst_branch ((fxs, assms), str) =
+      ((fxs, map (assume o cterm_of thy o inst_term o prop_of) assms),
+       inst_tree_aux str)
+  in
+    inst_tree_aux tr
+  end
 
 
 (* Poor man's contexts: Only fixes and assumes *)
 fun compose (fs1, as1) (fs2, as2) = (fs1 @ fs2, as1 @ as2)
 
 fun export_term (fixes, assumes) =
-    fold_rev (curry Logic.mk_implies o prop_of) assumes 
+ fold_rev (curry Logic.mk_implies o prop_of) assumes
  #> fold_rev (Logic.all o Free) fixes
 
 fun export_thm thy (fixes, assumes) =
-    fold_rev (implies_intr o cprop_of) assumes
+ fold_rev (implies_intr o cprop_of) assumes
  #> fold_rev (forall_intr o cterm_of thy o Free) fixes
 
 fun import_thm thy (fixes, athms) =
-    fold (forall_elim o cterm_of thy o Free) fixes
+ fold (forall_elim o cterm_of thy o Free) fixes
  #> fold Thm.elim_implies athms
 
 
 (* 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
-            
-      val (T, x) = fold fill_table (IntGraph.keys G) (Inttab.empty, x)
-    in
-      (Inttab.fold (cons o snd) T [], x)
-    end
-    
+  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
+
+    val (T, x) = fold fill_table (IntGraph.keys G) (Inttab.empty, x)
+  in
+    (Inttab.fold (cons o snd) T [], x)
+  end
+
 fun traverse_tree rcOp tr =
-    let 
-  fun traverse_help ctx (Leaf _) _ x = ([], x)
-    | traverse_help ctx (RCall (t, st)) u x =
-      rcOp ctx t u (traverse_help ctx st u x)
-    | traverse_help ctx (Cong (_, deps, branches)) u x =
+  let
+    fun traverse_help ctx (Leaf _) _ x = ([], x)
+      | traverse_help ctx (RCall (t, st)) u x =
+        rcOp ctx t u (traverse_help ctx st u x)
+      | traverse_help ctx (Cong (_, deps, branches)) u x =
       let
-    fun sub_step lu i x =
-        let
-          val (ctx', subtree) = nth branches i
-          val used = fold_rev (append o lu) (IntGraph.imm_succs deps i) u
-          val (subs, x') = traverse_help (compose ctx ctx') subtree used x
-          val exported_subs = map (apfst (compose ctx')) subs (* FIXME: Right order of composition? *)
-        in
-          (exported_subs, x')
-        end
+        fun sub_step lu i x =
+          let
+            val (ctx', subtree) = nth branches i
+            val used = fold_rev (append o lu) (IntGraph.imm_succs deps i) u
+            val (subs, x') = traverse_help (compose ctx ctx') subtree used x
+            val exported_subs = map (apfst (compose ctx')) subs (* FIXME: Right order of composition? *)
+          in
+            (exported_subs, x')
+          end
       in
         fold_deps deps sub_step x
-          |> apfst flat
+        |> apfst flat
       end
-    in
-      snd o traverse_help ([], []) tr []
-    end
+  in
+    snd o traverse_help ([], []) tr []
+  end
 
 fun rewrite_by_tree thy h ih x tr =
-    let
-      fun rewrite_help _ _ x (Leaf t) = (reflexive (cterm_of thy t), x)
-        | rewrite_help fix h_as x (RCall (_ $ arg, st)) =
-          let
-            val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *)
-                                                     
-            val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
-                 |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
+  let
+    fun rewrite_help _ _ x (Leaf t) = (reflexive (cterm_of thy t), x)
+      | rewrite_help fix h_as x (RCall (_ $ arg, st)) =
+        let
+          val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *)
+
+          val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
+            |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
                                                     (* (a, h a) : G   *)
-            val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
-            val eq = implies_elim (implies_elim inst_ih lRi) iha (* h a = f a *)
-                     
-            val h_a'_eq_h_a = combination (reflexive (cterm_of thy h)) inner
-            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 h_as x (Cong (crule, deps, branches)) =
-          let
-            fun sub_step lu i x =
-                let
-                  val ((fixes, assumes), st) = nth branches i
-                  val used = map lu (IntGraph.imm_succs deps i)
-                             |> map (fn u_eq => (u_eq RS sym) RS eq_reflection)
-                             |> filter_out Thm.is_reflexive
+          val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
+          val eq = implies_elim (implies_elim inst_ih lRi) iha (* h a = f a *)
+
+          val h_a'_eq_h_a = combination (reflexive (cterm_of thy h)) inner
+          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 h_as x (Cong (crule, deps, branches)) =
+        let
+          fun sub_step lu i x =
+            let
+              val ((fixes, assumes), st) = nth branches i
+              val used = map lu (IntGraph.imm_succs deps i)
+                |> map (fn u_eq => (u_eq RS sym) RS eq_reflection)
+                |> filter_out Thm.is_reflexive
 
-                  val assumes' = map (simplify (HOL_basic_ss addsimps used)) assumes
-                                 
-                  val (subeq, x') = rewrite_help (fix @ fixes) (h_as @ assumes') x st
-                  val subeq_exp = export_thm thy (fixes, 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
-    end
-    
+              val assumes' = map (simplify (HOL_basic_ss addsimps used)) assumes
+
+              val (subeq, x') =
+                rewrite_help (fix @ fixes) (h_as @ assumes') x st
+              val subeq_exp =
+                export_thm thy (fixes, 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
+  end
+
 end
--- a/src/HOL/Tools/Function/fun.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -7,14 +7,14 @@
 
 signature FUNCTION_FUN =
 sig
-    val add_fun : Function_Common.function_config ->
-      (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
-      bool -> local_theory -> Proof.context
-    val add_fun_cmd : Function_Common.function_config ->
-      (binding * string option * mixfix) list -> (Attrib.binding * string) list ->
-      bool -> local_theory -> Proof.context
+  val add_fun : Function_Common.function_config ->
+    (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
+    bool -> local_theory -> Proof.context
+  val add_fun_cmd : Function_Common.function_config ->
+    (binding * string option * mixfix) list -> (Attrib.binding * string) list ->
+    bool -> local_theory -> Proof.context
 
-    val setup : theory -> theory
+  val setup : theory -> theory
 end
 
 structure Function_Fun : FUNCTION_FUN =
@@ -25,64 +25,64 @@
 
 
 fun check_pats ctxt geq =
-    let 
-      fun err str = error (cat_lines ["Malformed definition:",
-                                      str ^ " not allowed in sequential mode.",
-                                      Syntax.string_of_term ctxt geq])
-      val thy = ProofContext.theory_of ctxt
-                
-      fun check_constr_pattern (Bound _) = ()
-        | check_constr_pattern t =
-          let
-            val (hd, args) = strip_comb t
-          in
-            (((case Datatype.info_of_constr thy (dest_Const hd) of
-                 SOME _ => ()
-               | NONE => err "Non-constructor pattern")
-              handle TERM ("dest_Const", _) => err "Non-constructor patterns");
-             map check_constr_pattern args; 
-             ())
-          end
-          
-      val (_, qs, gs, args, _) = split_def ctxt geq 
-                                       
-      val _ = if not (null gs) then err "Conditional equations" else ()
-      val _ = map check_constr_pattern args
-                  
-                  (* just count occurrences to check linearity *)
-      val _ = if fold (fold_aterms (fn Bound _ => Integer.add 1 | _ => I)) args 0 > length qs
-              then err "Nonlinear patterns" else ()
-    in
-      ()
-    end
-    
+  let
+    fun err str = error (cat_lines ["Malformed definition:",
+      str ^ " not allowed in sequential mode.",
+      Syntax.string_of_term ctxt geq])
+    val thy = ProofContext.theory_of ctxt
+
+    fun check_constr_pattern (Bound _) = ()
+      | check_constr_pattern t =
+      let
+        val (hd, args) = strip_comb t
+      in
+        (((case Datatype.info_of_constr thy (dest_Const hd) of
+             SOME _ => ()
+           | NONE => err "Non-constructor pattern")
+          handle TERM ("dest_Const", _) => err "Non-constructor patterns");
+         map check_constr_pattern args;
+         ())
+      end
+
+    val (_, qs, gs, args, _) = split_def ctxt geq
+
+    val _ = if not (null gs) then err "Conditional equations" else ()
+    val _ = map check_constr_pattern args
+
+    (* just count occurrences to check linearity *)
+    val _ = if fold (fold_aterms (fn Bound _ => Integer.add 1 | _ => I)) args 0 > length qs
+      then err "Nonlinear patterns" else ()
+  in
+    ()
+  end
+
 val by_pat_completeness_auto =
-    Proof.global_future_terminal_proof
-      (Method.Basic Pat_Completeness.pat_completeness,
-       SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
+  Proof.global_future_terminal_proof
+    (Method.Basic Pat_Completeness.pat_completeness,
+     SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
 
 fun termination_by method int =
-    Function.termination_proof NONE
-    #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int
+  Function.termination_proof NONE
+  #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int
 
 fun mk_catchall fixes arity_of =
-    let
-      fun mk_eqn ((fname, fT), _) =
-          let 
-            val n = arity_of fname
-            val (argTs, rT) = chop n (binder_types fT)
-                                   |> apsnd (fn Ts => Ts ---> body_type fT) 
-                              
-            val qs = map Free (Name.invent_list [] "a" n ~~ argTs)
-          in
-            HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
-                          Const ("HOL.undefined", rT))
-              |> HOLogic.mk_Trueprop
-              |> fold_rev Logic.all qs
-          end
-    in
-      map mk_eqn fixes
-    end
+  let
+    fun mk_eqn ((fname, fT), _) =
+      let
+        val n = arity_of fname
+        val (argTs, rT) = chop n (binder_types fT)
+          |> apsnd (fn Ts => Ts ---> body_type fT)
+
+        val qs = map Free (Name.invent_list [] "a" n ~~ argTs)
+      in
+        HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
+          Const ("HOL.undefined", rT))
+        |> HOLogic.mk_Trueprop
+        |> fold_rev Logic.all qs
+      end
+  in
+    map mk_eqn fixes
+  end
 
 fun add_catchall ctxt fixes spec =
   let val fqgars = map (split_def ctxt) spec
@@ -93,55 +93,53 @@
   end
 
 fun warn_if_redundant ctxt origs tss =
-    let
-        fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t)
-                    
-        val (tss', _) = chop (length origs) tss
-        fun check (t, []) = (warning (msg t); [])
-          | check (t, s) = s
-    in
-        (map check (origs ~~ tss'); tss)
-    end
+  let
+    fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t)
 
+    val (tss', _) = chop (length origs) tss
+    fun check (t, []) = (warning (msg t); [])
+      | check (t, s) = s
+  in
+    (map check (origs ~~ tss'); tss)
+  end
 
 fun sequential_preproc (config as FunctionConfig {sequential, ...}) ctxt fixes spec =
-      if sequential then
-        let
-          val (bnds, eqss) = split_list spec
-                            
-          val eqs = map the_single eqss
-                    
-          val feqs = eqs
-                      |> tap (check_defs ctxt fixes) (* Standard checks *)
-                      |> tap (map (check_pats ctxt))    (* More checks for sequential mode *)
+  if sequential then
+    let
+      val (bnds, eqss) = split_list spec
+
+      val eqs = map the_single eqss
 
-          val compleqs = add_catchall ctxt fixes feqs   (* Completion *)
+      val feqs = eqs
+        |> tap (check_defs ctxt fixes) (* Standard checks *)
+        |> tap (map (check_pats ctxt)) (* More checks for sequential mode *)
+
+      val compleqs = add_catchall ctxt fixes feqs (* Completion *)
 
-          val spliteqs = warn_if_redundant ctxt feqs
-                           (Function_Split.split_all_equations ctxt compleqs)
+      val spliteqs = warn_if_redundant ctxt feqs
+        (Function_Split.split_all_equations ctxt compleqs)
+
+      fun restore_spec thms =
+        bnds ~~ take (length bnds) (unflat spliteqs thms)
 
-          fun restore_spec thms =
-              bnds ~~ take (length bnds) (unflat spliteqs thms)
-              
-          val spliteqs' = flat (take (length bnds) spliteqs)
-          val fnames = map (fst o fst) fixes
-          val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'
+      val spliteqs' = flat (take (length bnds) spliteqs)
+      val fnames = map (fst o fst) fixes
+      val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'
 
-          fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs)
-                                       |> map (map snd)
+      fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs)
+        |> map (map snd)
 
 
-          val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding
+      val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding
 
-          (* using theorem names for case name currently disabled *)
-          val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es)) 
-                                     (bnds' ~~ spliteqs)
-                           |> flat
-        in
-          (flat spliteqs, restore_spec, sort, case_names)
-        end
-      else
-        Function_Common.empty_preproc check_defs config ctxt fixes spec
+      (* using theorem names for case name currently disabled *)
+      val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es)) 
+        (bnds' ~~ spliteqs) |> flat
+    in
+      (flat spliteqs, restore_spec, sort, case_names)
+    end
+  else
+    Function_Common.empty_preproc check_defs config ctxt fixes spec
 
 val setup =
   Context.theory_map (Function_Common.set_preproc sequential_preproc)
@@ -152,10 +150,10 @@
 
 fun gen_fun add config fixes statements int lthy =
   lthy
-    |> add fixes statements config
-    |> by_pat_completeness_auto int
-    |> Local_Theory.restore
-    |> termination_by (Function_Common.get_termination_prover lthy) int
+  |> add fixes statements config
+  |> by_pat_completeness_auto int
+  |> Local_Theory.restore
+  |> termination_by (Function_Common.get_termination_prover lthy) int
 
 val add_fun = gen_fun Function.add_function
 val add_fun_cmd = gen_fun Function.add_function_cmd
--- a/src/HOL/Tools/Function/function.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/function.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -7,26 +7,23 @@
 
 signature FUNCTION =
 sig
-    include FUNCTION_DATA
+  include FUNCTION_DATA
+
+  val add_function: (binding * typ option * mixfix) list ->
+    (Attrib.binding * term) list -> Function_Common.function_config ->
+    local_theory -> Proof.state
 
-    val add_function :  (binding * typ option * mixfix) list
-                       -> (Attrib.binding * term) list
-                       -> Function_Common.function_config
-                       -> local_theory
-                       -> Proof.state
-    val add_function_cmd :  (binding * string option * mixfix) list
-                      -> (Attrib.binding * string) list
-                      -> Function_Common.function_config
-                      -> local_theory
-                      -> Proof.state
+  val add_function_cmd: (binding * string option * mixfix) list ->
+    (Attrib.binding * string) list -> Function_Common.function_config ->
+    local_theory -> Proof.state
 
-    val termination_proof : term option -> local_theory -> Proof.state
-    val termination_proof_cmd : string option -> local_theory -> Proof.state
+  val termination_proof : term option -> local_theory -> Proof.state
+  val termination_proof_cmd : string option -> local_theory -> Proof.state
 
-    val setup : theory -> theory
-    val get_congs : Proof.context -> thm list
+  val setup : theory -> theory
+  val get_congs : Proof.context -> thm list
 
-    val get_info : Proof.context -> term -> info
+  val get_info : Proof.context -> term -> info
 end
 
 
@@ -37,148 +34,149 @@
 open Function_Common
 
 val simp_attribs = map (Attrib.internal o K)
-    [Simplifier.simp_add,
-     Code.add_default_eqn_attribute,
-     Nitpick_Simps.add]
+  [Simplifier.simp_add,
+   Code.add_default_eqn_attribute,
+   Nitpick_Simps.add]
 
 val psimp_attribs = map (Attrib.internal o K)
-    [Simplifier.simp_add,
-     Nitpick_Psimps.add]
+  [Simplifier.simp_add,
+   Nitpick_Psimps.add]
 
 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
 
-fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy =
-    let
-      val spec = post simps
-                   |> map (apfst (apsnd (fn ats => moreatts @ ats)))
-                   |> map (apfst (apfst extra_qualify))
+fun add_simps fnames post sort extra_qualify label mod_binding moreatts
+  simps lthy =
+  let
+    val spec = post simps
+      |> map (apfst (apsnd (fn ats => moreatts @ ats)))
+      |> map (apfst (apfst extra_qualify))
 
-      val (saved_spec_simps, lthy) =
-        fold_map Local_Theory.note spec lthy
+    val (saved_spec_simps, lthy) =
+      fold_map Local_Theory.note spec lthy
 
-      val saved_simps = maps snd saved_spec_simps
-      val simps_by_f = sort saved_simps
+    val saved_simps = maps snd saved_spec_simps
+    val simps_by_f = sort saved_simps
 
-      fun add_for_f fname simps =
-        Local_Theory.note
-          ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
-        #> snd
-    in
-      (saved_simps,
-       fold2 add_for_f fnames simps_by_f lthy)
-    end
+    fun add_for_f fname simps =
+      Local_Theory.note
+        ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
+      #> snd
+  in
+    (saved_simps, fold2 add_for_f fnames simps_by_f lthy)
+  end
 
 fun gen_add_function is_external prep default_constraint fixspec eqns config lthy =
-    let
-      val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
-      val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
-      val fixes = map (apfst (apfst Binding.name_of)) fixes0;
-      val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
-      val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
+  let
+    val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
+    val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
+    val fixes = map (apfst (apfst Binding.name_of)) fixes0;
+    val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
+    val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
 
-      val defname = mk_defname fixes
-      val FunctionConfig {partials, ...} = config
+    val defname = mk_defname fixes
+    val FunctionConfig {partials, ...} = config
 
-      val ((goalstate, cont), lthy) =
-          Function_Mutual.prepare_function_mutual config defname fixes eqs lthy
+    val ((goalstate, cont), lthy) =
+      Function_Mutual.prepare_function_mutual config defname fixes eqs lthy
 
-      fun afterqed [[proof]] lthy =
-        let
-          val FunctionResult {fs, R, psimps, trsimps,  simple_pinducts, termination,
-                            domintros, cases, ...} =
+    fun afterqed [[proof]] lthy =
+      let
+        val FunctionResult {fs, R, psimps, trsimps,  simple_pinducts,
+          termination, domintros, cases, ...} =
           cont (Thm.close_derivation proof)
 
-          val fnames = map (fst o fst) fixes
-          fun qualify n = Binding.name n
-            |> Binding.qualify true defname
-          val conceal_partial = if partials then I else Binding.conceal
+        val fnames = map (fst o fst) fixes
+        fun qualify n = Binding.name n
+          |> Binding.qualify true defname
+        val conceal_partial = if partials then I else Binding.conceal
 
-          val addsmps = add_simps fnames post sort_cont
+        val addsmps = add_simps fnames post sort_cont
 
-          val (((psimps', pinducts'), (_, [termination'])), lthy) =
-            lthy
-            |> addsmps (conceal_partial o Binding.qualify false "partial")
-                 "psimps" conceal_partial psimp_attribs psimps
-            ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
-            ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
-                   [Attrib.internal (K (Rule_Cases.case_names cnames)),
-                    Attrib.internal (K (Rule_Cases.consumes 1)),
-                    Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
-            ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
-            ||> (snd o Local_Theory.note ((qualify "cases",
-                   [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
-            ||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros
+        val (((psimps', pinducts'), (_, [termination'])), lthy) =
+          lthy
+          |> addsmps (conceal_partial o Binding.qualify false "partial")
+               "psimps" conceal_partial psimp_attribs psimps
+          ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
+          ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
+                 [Attrib.internal (K (Rule_Cases.case_names cnames)),
+                  Attrib.internal (K (Rule_Cases.consumes 1)),
+                  Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
+          ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
+          ||> (snd o Local_Theory.note ((qualify "cases",
+                 [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
+          ||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros
 
-          val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
-            pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
-            fs=fs, R=R, defname=defname, is_partial=true }
+        val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
+          pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
+          fs=fs, R=R, defname=defname, is_partial=true }
 
-          val _ =
-            if not is_external then ()
-            else Specification.print_consts lthy (K false) (map fst fixes)
-        in
-          lthy
-          |> Local_Theory.declaration false (add_function_data o morph_function_data info)
-        end
-    in
-      lthy
-        |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
-        |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
-    end
+        val _ =
+          if not is_external then ()
+          else Specification.print_consts lthy (K false) (map fst fixes)
+      in
+        lthy
+        |> Local_Theory.declaration false (add_function_data o morph_function_data info)
+      end
+  in
+    lthy
+    |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
+    |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
+  end
 
-val add_function = gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
+val add_function =
+  gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
 val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
 
 fun gen_termination_proof prep_term raw_term_opt lthy =
-    let
-      val term_opt = Option.map (prep_term lthy) raw_term_opt
-      val info = the (case term_opt of
-                        SOME t => (import_function_data t lthy
-                          handle Option.Option =>
-                            error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
-                      | NONE => (import_last_function lthy handle Option.Option => error "Not a function"))
+  let
+    val term_opt = Option.map (prep_term lthy) raw_term_opt
+    val info = the (case term_opt of
+                      SOME t => (import_function_data t lthy
+                        handle Option.Option =>
+                          error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
+                    | NONE => (import_last_function lthy handle Option.Option => error "Not a function"))
 
-        val { termination, fs, R, add_simps, case_names, psimps,
-          pinducts, defname, ...} = info
-        val domT = domain_type (fastype_of R)
-        val goal = HOLogic.mk_Trueprop
-                     (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
-        fun afterqed [[totality]] lthy =
-          let
-            val totality = Thm.close_derivation totality
-            val remove_domain_condition =
-              full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
-            val tsimps = map remove_domain_condition psimps
-            val tinduct = map remove_domain_condition pinducts
+      val { termination, fs, R, add_simps, case_names, psimps,
+        pinducts, defname, ...} = info
+      val domT = domain_type (fastype_of R)
+      val goal = HOLogic.mk_Trueprop
+                   (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
+      fun afterqed [[totality]] lthy =
+        let
+          val totality = Thm.close_derivation totality
+          val remove_domain_condition =
+            full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
+          val tsimps = map remove_domain_condition psimps
+          val tinduct = map remove_domain_condition pinducts
 
-            fun qualify n = Binding.name n
-              |> Binding.qualify true defname
-          in
-            lthy
-            |> add_simps I "simps" I simp_attribs tsimps
-            ||>> Local_Theory.note
-               ((qualify "induct",
-                 [Attrib.internal (K (Rule_Cases.case_names case_names))]),
-                tinduct)
-            |-> (fn (simps, (_, inducts)) =>
-              let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
-                case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
-                simps=SOME simps, inducts=SOME inducts, termination=termination }
-              in
-                Local_Theory.declaration false (add_function_data o morph_function_data info')
-              end)
-          end
-    in
-      lthy
-      |> ProofContext.note_thmss ""
-         [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
-      |> ProofContext.note_thmss ""
-         [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
-      |> ProofContext.note_thmss ""
-         [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
-           [([Goal.norm_result termination], [])])] |> snd
-      |> Proof.theorem_i NONE afterqed [[(goal, [])]]
-    end
+          fun qualify n = Binding.name n
+            |> Binding.qualify true defname
+        in
+          lthy
+          |> add_simps I "simps" I simp_attribs tsimps
+          ||>> Local_Theory.note
+             ((qualify "induct",
+               [Attrib.internal (K (Rule_Cases.case_names case_names))]),
+              tinduct)
+          |-> (fn (simps, (_, inducts)) =>
+            let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
+              case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
+              simps=SOME simps, inducts=SOME inducts, termination=termination }
+            in
+              Local_Theory.declaration false (add_function_data o morph_function_data info')
+            end)
+        end
+  in
+    lthy
+    |> ProofContext.note_thmss ""
+       [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
+    |> ProofContext.note_thmss ""
+       [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
+    |> ProofContext.note_thmss ""
+       [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
+         [([Goal.norm_result termination], [])])] |> snd
+    |> Proof.theorem_i NONE afterqed [[(goal, [])]]
+  end
 
 val termination_proof = gen_termination_proof Syntax.check_term
 val termination_proof_cmd = gen_termination_proof Syntax.read_term
@@ -188,11 +186,13 @@
 
 
 fun add_case_cong n thy =
-    Context.theory_map (Function_Ctx_Tree.map_function_congs (Thm.add_thm
-                          (Datatype.the_info thy n
-                           |> #case_cong
-                           |> safe_mk_meta_eq)))
-                       thy
+  let
+    val cong = #case_cong (Datatype.the_info thy n)
+      |> safe_mk_meta_eq
+  in
+    Context.theory_map
+      (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy
+  end
 
 val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))
 
--- a/src/HOL/Tools/Function/function_common.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -1,7 +1,7 @@
-(*  Title:      HOL/Tools/Function/fundef_common.ML
+(*  Title:      HOL/Tools/Function/function_common.ML
     Author:     Alexander Krauss, TU Muenchen
 
-A package for general recursive function definitions. 
+A package for general recursive function definitions.
 Common definitions and other infrastructure.
 *)
 
@@ -21,8 +21,7 @@
   pinducts: thm list,
   simps : thm list option,
   inducts : thm list option,
-  termination: thm
- }  
+  termination: thm}
 
 end
 
@@ -42,8 +41,7 @@
   pinducts: thm list,
   simps : thm list option,
   inducts : thm list option,
-  termination: thm
- }  
+  termination: thm}
 
 end
 
@@ -62,7 +60,7 @@
 
 val acc_const_name = @{const_name accp}
 fun mk_acc domT R =
-    Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
+  Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
 
 val function_name = suffix "C"
 val graph_name = suffix "_graph"
@@ -86,21 +84,18 @@
 
 (* Function definition result data *)
 
-datatype function_result =
-  FunctionResult of
-     {
-      fs: term list,
-      G: term,
-      R: term,
+datatype function_result = FunctionResult of
+ {fs: term list,
+  G: term,
+  R: term,
 
-      psimps : thm list, 
-      trsimps : thm list option, 
+  psimps : thm list,
+  trsimps : thm list option,
 
-      simple_pinducts : thm list, 
-      cases : thm,
-      termination : thm,
-      domintros : thm list option
-     }
+  simple_pinducts : thm list,
+  cases : thm,
+  termination : thm,
+  domintros : thm list option}
 
 fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
   simps, inducts, termination, defname, is_partial} : info) phi =
@@ -109,7 +104,7 @@
       val name = Binding.name_of o Morphism.binding phi o Binding.name
     in
       { add_simps = add_simps, case_names = case_names,
-        fs = map term fs, R = term R, psimps = fact psimps, 
+        fs = map term fs, R = term R, psimps = fact psimps,
         pinducts = fact pinducts, simps = Option.map fact simps,
         inducts = Option.map fact inducts, termination = thm termination,
         defname = name defname, is_partial=is_partial }
@@ -121,57 +116,56 @@
   val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
   val extend = I;
   fun merge tabs : T = Item_Net.merge tabs;
-);
+)
 
 val get_function = FunctionData.get o Context.Proof;
 
 
-(* Generally useful?? *)
-fun lift_morphism thy f = 
-    let 
-      val term = Drule.term_rule thy f
-    in
-      Morphism.thm_morphism f $> Morphism.term_morphism term 
-       $> Morphism.typ_morphism (Logic.type_map term)
-    end
+fun lift_morphism thy f =
+  let
+    val term = Drule.term_rule thy f
+  in
+    Morphism.thm_morphism f $> Morphism.term_morphism term
+    $> Morphism.typ_morphism (Logic.type_map term)
+  end
 
 fun import_function_data t ctxt =
-    let
-      val thy = ProofContext.theory_of ctxt
-      val ct = cterm_of thy t
-      val inst_morph = lift_morphism thy o Thm.instantiate 
+  let
+    val thy = ProofContext.theory_of ctxt
+    val ct = cterm_of thy t
+    val inst_morph = lift_morphism thy o Thm.instantiate
 
-      fun match (trm, data) = 
-          SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
-          handle Pattern.MATCH => NONE
-    in 
-      get_first match (Item_Net.retrieve (get_function ctxt) t)
-    end
+    fun match (trm, data) =
+      SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
+      handle Pattern.MATCH => NONE
+  in
+    get_first match (Item_Net.retrieve (get_function ctxt) t)
+  end
 
 fun import_last_function ctxt =
-    case Item_Net.content (get_function ctxt) of
-      [] => NONE
-    | (t, data) :: _ =>
-      let 
-        val ([t'], ctxt') = Variable.import_terms true [t] ctxt
-      in
-        import_function_data t' ctxt'
-      end
+  case Item_Net.content (get_function ctxt) of
+    [] => NONE
+  | (t, data) :: _ =>
+    let
+      val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+    in
+      import_function_data t' ctxt'
+    end
 
 val all_function_data = Item_Net.content o get_function
 
 fun add_function_data (data : info as {fs, termination, ...}) =
-    FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
-    #> store_termination_rule termination
+  FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
+  #> store_termination_rule termination
 
 
 (* Simp rules for termination proofs *)
 
 structure Termination_Simps = Named_Thms
 (
-  val name = "termination_simp" 
+  val name = "termination_simp"
   val description = "Simplification rule for termination proofs"
-);
+)
 
 
 (* Default Termination Prover *)
@@ -182,29 +176,26 @@
   val empty = (fn _ => error "Termination prover not configured")
   val extend = I
   fun merge (a, b) = b  (* FIXME ? *)
-);
+)
 
 val set_termination_prover = TerminationProver.put
 val get_termination_prover = TerminationProver.get o Context.Proof
 
 
 (* Configuration management *)
-datatype function_opt 
+datatype function_opt
   = Sequential
   | Default of string
   | DomIntros
   | No_Partials
   | Tailrec
 
-datatype function_config
-  = FunctionConfig of
-   {
-    sequential: bool,
-    default: string,
-    domintros: bool,
-    partials: bool,
-    tailrec: bool
-   }
+datatype function_config = FunctionConfig of
+ {sequential: bool,
+  default: string,
+  domintros: bool,
+  partials: bool,
+  tailrec: bool}
 
 fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
     FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials, tailrec=tailrec}
@@ -225,97 +216,94 @@
 (* Analyzing function equations *)
 
 fun split_def ctxt geq =
-    let
-      fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
-      val qs = Term.strip_qnt_vars "all" geq
-      val imp = Term.strip_qnt_body "all" geq
-      val (gs, eq) = Logic.strip_horn imp
+  let
+    fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
+    val qs = Term.strip_qnt_vars "all" geq
+    val imp = Term.strip_qnt_body "all" geq
+    val (gs, eq) = Logic.strip_horn imp
 
-      val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
-          handle TERM _ => error (input_error "Not an equation")
+    val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
+      handle TERM _ => error (input_error "Not an equation")
 
-      val (head, args) = strip_comb f_args
+    val (head, args) = strip_comb f_args
 
-      val fname = fst (dest_Free head)
-          handle TERM _ => error (input_error "Head symbol must not be a bound variable")
-    in
-      (fname, qs, gs, args, rhs)
-    end
+    val fname = fst (dest_Free head)
+      handle TERM _ => error (input_error "Head symbol must not be a bound variable")
+  in
+    (fname, qs, gs, args, rhs)
+  end
 
 (* Check for all sorts of errors in the input *)
 fun check_defs ctxt fixes eqs =
-    let
-      val fnames = map (fst o fst) fixes
-                                
-      fun check geq = 
-          let
-            fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
-                                  
-            val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
-                                 
-            val _ = fname mem fnames 
-                    orelse input_error 
-                             ("Head symbol of left hand side must be " 
-                              ^ plural "" "one out of " fnames ^ commas_quote fnames)
-                                            
-            val _ = length args > 0 orelse input_error "Function has no arguments:"
+  let
+    val fnames = map (fst o fst) fixes
+
+    fun check geq =
+      let
+        fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
 
-            fun add_bvs t is = add_loose_bnos (t, 0, is)
+        val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
+
+        val _ = fname mem fnames
+          orelse input_error ("Head symbol of left hand side must be " ^
+            plural "" "one out of " fnames ^ commas_quote fnames)
+
+        val _ = length args > 0 orelse input_error "Function has no arguments:"
+
+        fun add_bvs t is = add_loose_bnos (t, 0, is)
             val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
                         |> map (fst o nth (rev qs))
-                      
-            val _ = null rvs orelse input_error 
-                        ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
-                         ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
-                                    
-            val _ = forall (not o Term.exists_subterm 
-                             (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args)
-                    orelse input_error "Defined function may not occur in premises or arguments"
+
+        val _ = null rvs orelse input_error
+          ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^
+           " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
+
+        val _ = forall (not o Term.exists_subterm
+          (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args)
+          orelse input_error "Defined function may not occur in premises or arguments"
 
-            val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
-            val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
-            val _ = null funvars
-                    orelse (warning (cat_lines 
-                    ["Bound variable" ^ plural " " "s " funvars 
-                     ^ commas_quote (map fst funvars) ^  
-                     " occur" ^ plural "s" "" funvars ^ " in function position.",  
-                     "Misspelled constructor???"]); true)
-          in
-            (fname, length args)
-          end
+        val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
+        val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
+        val _ = null funvars orelse (warning (cat_lines
+          ["Bound variable" ^ plural " " "s " funvars ^
+          commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^
+          " in function position.", "Misspelled constructor???"]); true)
+      in
+        (fname, length args)
+      end
 
-      val grouped_args = AList.group (op =) (map check eqs)
-      val _ = grouped_args
-        |> map (fn (fname, ars) =>
-             length (distinct (op =) ars) = 1
-             orelse error ("Function " ^ quote fname ^
-                           " has different numbers of arguments in different equations"))
+    val grouped_args = AList.group (op =) (map check eqs)
+    val _ = grouped_args
+      |> map (fn (fname, ars) =>
+        length (distinct (op =) ars) = 1
+        orelse error ("Function " ^ quote fname ^
+          " has different numbers of arguments in different equations"))
 
-      val not_defined = subtract (op =) (map fst grouped_args) fnames
-      val _ = null not_defined
-        orelse error ("No defining equations for function" ^
-          plural " " "s " not_defined ^ commas_quote not_defined)
+    val not_defined = subtract (op =) (map fst grouped_args) fnames
+    val _ = null not_defined
+      orelse error ("No defining equations for function" ^
+        plural " " "s " not_defined ^ commas_quote not_defined)
 
-      fun check_sorts ((fname, fT), _) =
-          Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
-          orelse error (cat_lines 
-          ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
-           setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
+    fun check_sorts ((fname, fT), _) =
+      Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
+      orelse error (cat_lines
+      ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
+       setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
 
-      val _ = map check_sorts fixes
-    in
-      ()
-    end
+    val _ = map check_sorts fixes
+  in
+    ()
+  end
 
 (* Preprocessors *)
 
 type fixes = ((string * typ) * mixfix) list
 type 'a spec = (Attrib.binding * 'a list) list
-type preproc = function_config -> Proof.context -> fixes -> term spec 
-               -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
+type preproc = function_config -> Proof.context -> fixes -> term spec ->
+  (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
 
-val fname_of = fst o dest_Free o fst o strip_comb o fst 
- o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
+val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o
+  HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
 
 fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
   | mk_case_names _ n 0 = []
@@ -323,22 +311,21 @@
   | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
 
 fun empty_preproc check _ ctxt fixes spec =
-    let 
-      val (bnds, tss) = split_list spec
-      val ts = flat tss
-      val _ = check ctxt fixes ts
-      val fnames = map (fst o fst) fixes
-      val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
+  let
+    val (bnds, tss) = split_list spec
+    val ts = flat tss
+    val _ = check ctxt fixes ts
+    val fnames = map (fst o fst) fixes
+    val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
 
-      fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 
-                                   (indices ~~ xs)
-                        |> map (map snd)
+    fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 
+      (indices ~~ xs) |> map (map snd)
 
-      (* using theorem names for case name currently disabled *)
-      val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
-    in
-      (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
-    end
+    (* using theorem names for case name currently disabled *)
+    val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
+  in
+    (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
+  end
 
 structure Preprocessor = Generic_Data
 (
@@ -346,32 +333,31 @@
   val empty : T = empty_preproc check_defs
   val extend = I
   fun merge (a, _) = a
-);
+)
 
 val get_preproc = Preprocessor.get o Context.Proof
 val set_preproc = Preprocessor.map o K
 
 
 
-local 
+local
   structure P = OuterParse and K = OuterKeyword
 
-  val option_parser = 
-      P.group "option" ((P.reserved "sequential" >> K Sequential)
-                    || ((P.reserved "default" |-- P.term) >> Default)
-                    || (P.reserved "domintros" >> K DomIntros)
-                    || (P.reserved "no_partials" >> K No_Partials)
-                    || (P.reserved "tailrec" >> K Tailrec))
+  val option_parser = P.group "option"
+    ((P.reserved "sequential" >> K Sequential)
+     || ((P.reserved "default" |-- P.term) >> Default)
+     || (P.reserved "domintros" >> K DomIntros)
+     || (P.reserved "no_partials" >> K No_Partials)
+     || (P.reserved "tailrec" >> K Tailrec))
 
-  fun config_parser default = 
-      (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
-        >> (fn opts => fold apply_opt opts default)
+  fun config_parser default =
+    (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
+     >> (fn opts => fold apply_opt opts default)
 in
-  fun function_parser default_cfg = 
+  fun function_parser default_cfg =
       config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs
 end
 
 
 end
 end
-
--- a/src/HOL/Tools/Function/function_core.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -7,26 +7,25 @@
 
 signature FUNCTION_CORE =
 sig
-    val trace: bool Unsynchronized.ref
+  val trace: bool Unsynchronized.ref
 
-    val prepare_function : Function_Common.function_config
-                         -> string (* defname *)
-                         -> ((bstring * typ) * mixfix) list (* defined symbol *)
-                         -> ((bstring * typ) list * term list * term * term) list (* specification *)
-                         -> local_theory
-
-                         -> (term   (* f *)
-                             * thm  (* goalstate *)
-                             * (thm -> Function_Common.function_result) (* continuation *)
-                            ) * local_theory
+  val prepare_function : Function_Common.function_config
+    -> string (* defname *)
+    -> ((bstring * typ) * mixfix) list (* defined symbol *)
+    -> ((bstring * typ) list * term list * term * term) list (* specification *)
+    -> local_theory
+    -> (term   (* f *)
+        * thm  (* goalstate *)
+        * (thm -> Function_Common.function_result) (* continuation *)
+       ) * local_theory
 
 end
 
 structure Function_Core : FUNCTION_CORE =
 struct
 
-val trace = Unsynchronized.ref false;
-fun trace_msg msg = if ! trace then tracing (msg ()) else ();
+val trace = Unsynchronized.ref false
+fun trace_msg msg = if ! trace then tracing (msg ()) else ()
 
 val boolT = HOLogic.boolT
 val mk_eq = HOLogic.mk_eq
@@ -34,149 +33,134 @@
 open Function_Lib
 open Function_Common
 
-datatype globals =
-   Globals of {
-         fvar: term,
-         domT: typ,
-         ranT: typ,
-         h: term,
-         y: term,
-         x: term,
-         z: term,
-         a: term,
-         P: term,
-         D: term,
-         Pbool:term
-}
+datatype globals = Globals of
+ {fvar: term,
+  domT: typ,
+  ranT: typ,
+  h: term,
+  y: term,
+  x: term,
+  z: term,
+  a: term,
+  P: term,
+  D: term,
+  Pbool:term}
+
+datatype rec_call_info = RCInfo of
+ {RIvs: (string * typ) list,  (* Call context: fixes and assumes *)
+  CCas: thm list,
+  rcarg: term,                 (* The recursive argument *)
+  llRI: thm,
+  h_assum: term}
 
 
-datatype rec_call_info =
-  RCInfo of
-  {
-   RIvs: (string * typ) list,  (* Call context: fixes and assumes *)
-   CCas: thm list,
-   rcarg: term,                 (* The recursive argument *)
-
-   llRI: thm,
-   h_assum: term
-  }
-
-
-datatype clause_context =
-  ClauseContext of
-  {
-    ctxt : Proof.context,
-
-    qs : term list,
-    gs : term list,
-    lhs: term,
-    rhs: term,
-
-    cqs: cterm list,
-    ags: thm list,
-    case_hyp : thm
-  }
+datatype clause_context = ClauseContext of
+ {ctxt : Proof.context,
+  qs : term list,
+  gs : term list,
+  lhs: term,
+  rhs: term,
+  cqs: cterm list,
+  ags: thm list,
+  case_hyp : thm}
 
 
 fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
-    ClauseContext { ctxt = ProofContext.transfer thy ctxt,
-                    qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
+  ClauseContext { ctxt = ProofContext.transfer thy ctxt,
+    qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
 
 
-datatype clause_info =
-  ClauseInfo of
-     {
-      no: int,
-      qglr : ((string * typ) list * term list * term * term),
-      cdata : clause_context,
-
-      tree: Function_Ctx_Tree.ctx_tree,
-      lGI: thm,
-      RCs: rec_call_info list
-     }
+datatype clause_info = ClauseInfo of
+ {no: int,
+  qglr : ((string * typ) list * term list * term * term),
+  cdata : clause_context,
+  tree: Function_Ctx_Tree.ctx_tree,
+  lGI: thm,
+  RCs: rec_call_info list}
 
 
 (* Theory dependencies. *)
-val acc_induct_rule = @{thm accp_induct_rule};
+val acc_induct_rule = @{thm accp_induct_rule}
 
-val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence};
-val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness};
-val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff};
+val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}
+val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}
+val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff}
 
-val acc_downward = @{thm accp_downward};
-val accI = @{thm accp.accI};
-val case_split = @{thm HOL.case_split};
-val fundef_default_value = @{thm FunDef.fundef_default_value};
-val not_acc_down = @{thm not_accp_down};
+val acc_downward = @{thm accp_downward}
+val accI = @{thm accp.accI}
+val case_split = @{thm HOL.case_split}
+val fundef_default_value = @{thm FunDef.fundef_default_value}
+val not_acc_down = @{thm not_accp_down}
 
 
 
 fun find_calls tree =
-    let
-      fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
-        | add_Ri _ _ _ _ = raise Match
-    in
-      rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
-    end
+  let
+    fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) =
+      ([], (fixes, assumes, arg) :: xs)
+      | add_Ri _ _ _ _ = raise Match
+  in
+    rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
+  end
 
 
 (** building proof obligations *)
 
 fun mk_compat_proof_obligations domT ranT fvar f glrs =
-    let
-      fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
-          let
-            val shift = incr_boundvars (length qs')
-          in
-            Logic.mk_implies
-              (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
-                HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
-              |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
-              |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
-              |> curry abstract_over fvar
-              |> curry subst_bound f
-          end
-    in
-      map mk_impl (unordered_pairs glrs)
-    end
+  let
+    fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
+      let
+        val shift = incr_boundvars (length qs')
+      in
+        Logic.mk_implies
+          (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
+            HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
+        |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
+        |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
+        |> curry abstract_over fvar
+        |> curry subst_bound f
+      end
+  in
+    map mk_impl (unordered_pairs glrs)
+  end
 
 
 fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
-    let
-        fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
-            HOLogic.mk_Trueprop Pbool
-                     |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))
-                     |> fold_rev (curry Logic.mk_implies) gs
-                     |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
-    in
-        HOLogic.mk_Trueprop Pbool
-                 |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
-                 |> mk_forall_rename ("x", x)
-                 |> mk_forall_rename ("P", Pbool)
-    end
+  let
+    fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
+      HOLogic.mk_Trueprop Pbool
+      |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))
+      |> fold_rev (curry Logic.mk_implies) gs
+      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+  in
+    HOLogic.mk_Trueprop Pbool
+    |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
+    |> mk_forall_rename ("x", x)
+    |> mk_forall_rename ("P", Pbool)
+  end
 
 (** making a context with it's own local bindings **)
 
 fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
-    let
-      val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
-                                           |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
+  let
+    val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
+      |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
 
-      val thy = ProofContext.theory_of ctxt'
+    val thy = ProofContext.theory_of ctxt'
 
-      fun inst t = subst_bounds (rev qs, t)
-      val gs = map inst pre_gs
-      val lhs = inst pre_lhs
-      val rhs = inst pre_rhs
+    fun inst t = subst_bounds (rev qs, t)
+    val gs = map inst pre_gs
+    val lhs = inst pre_lhs
+    val rhs = inst pre_rhs
 
-      val cqs = map (cterm_of thy) qs
-      val ags = map (assume o cterm_of thy) gs
+    val cqs = map (cterm_of thy) qs
+    val ags = map (assume o cterm_of thy) gs
 
-      val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
-    in
-      ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
-                      cqs = cqs, ags = ags, case_hyp = case_hyp }
-    end
+    val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
+  in
+    ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
+      cqs = cqs, ags = ags, case_hyp = case_hyp }
+  end
 
 
 (* lowlevel term function. FIXME: remove *)
@@ -188,7 +172,7 @@
         (case tm of
           Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
         | t $ u => abs lev v t $ abs lev v u
-        | t => t);
+        | t => t)
   in
     fold_index (fn (i, v) => fn t => abs i v t) vs body
   end
@@ -196,258 +180,249 @@
 
 
 fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
-    let
-        val Globals {h, ...} = globals
+  let
+    val Globals {h, ...} = globals
 
-        val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
-        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
+    val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
+    val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
 
-        (* Instantiate the GIntro thm with "f" and import into the clause context. *)
-        val lGI = GIntro_thm
-                    |> forall_elim (cert f)
-                    |> fold forall_elim cqs
-                    |> fold Thm.elim_implies ags
-
-        fun mk_call_info (rcfix, rcassm, rcarg) RI =
-            let
-                val llRI = RI
-                             |> fold forall_elim cqs
-                             |> fold (forall_elim o cert o Free) rcfix
-                             |> fold Thm.elim_implies ags
-                             |> fold Thm.elim_implies rcassm
+    (* Instantiate the GIntro thm with "f" and import into the clause context. *)
+    val lGI = GIntro_thm
+      |> forall_elim (cert f)
+      |> fold forall_elim cqs
+      |> fold Thm.elim_implies ags
 
-                val h_assum =
-                    HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
-                              |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
-                              |> fold_rev (Logic.all o Free) rcfix
-                              |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
-                              |> abstract_over_list (rev qs)
-            in
-                RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
-            end
+    fun mk_call_info (rcfix, rcassm, rcarg) RI =
+      let
+        val llRI = RI
+          |> fold forall_elim cqs
+          |> fold (forall_elim o cert o Free) rcfix
+          |> fold Thm.elim_implies ags
+          |> fold Thm.elim_implies rcassm
 
-        val RC_infos = map2 mk_call_info RCs RIntro_thms
-    in
-        ClauseInfo
-            {
-             no=no,
-             cdata=cdata,
-             qglr=qglr,
+        val h_assum =
+          HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
+          |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+          |> fold_rev (Logic.all o Free) rcfix
+          |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
+          |> abstract_over_list (rev qs)
+      in
+        RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
+      end
 
-             lGI=lGI,
-             RCs=RC_infos,
-             tree=tree
-            }
-    end
+    val RC_infos = map2 mk_call_info RCs RIntro_thms
+  in
+    ClauseInfo {no=no, cdata=cdata, qglr=qglr, lGI=lGI, RCs=RC_infos,
+      tree=tree}
+  end
 
 
-
-
-
-
-
-(* replace this by a table later*)
 fun store_compat_thms 0 thms = []
   | store_compat_thms n thms =
-    let
-        val (thms1, thms2) = chop n thms
-    in
-        (thms1 :: store_compat_thms (n - 1) thms2)
-    end
+  let
+    val (thms1, thms2) = chop n thms
+  in
+    (thms1 :: store_compat_thms (n - 1) thms2)
+  end
 
 (* expects i <= j *)
 fun lookup_compat_thm i j cts =
-    nth (nth cts (i - 1)) (j - i)
+  nth (nth cts (i - 1)) (j - i)
 
 (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
 (* if j < i, then turn around *)
 fun get_compat_thm thy cts i j ctxi ctxj =
-    let
-      val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
-      val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
+  let
+    val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
+    val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
 
-      val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
-    in if j < i then
-         let
-           val compat = lookup_compat_thm j i cts
-         in
-           compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
-                |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
-                |> fold Thm.elim_implies agsj
-                |> fold Thm.elim_implies agsi
-                |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
-         end
-       else
-         let
-           val compat = lookup_compat_thm i j cts
-         in
-               compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
-                 |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
-                 |> fold Thm.elim_implies agsi
-                 |> fold Thm.elim_implies agsj
-                 |> Thm.elim_implies (assume lhsi_eq_lhsj)
-                 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
-         end
+    val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
+  in if j < i then
+    let
+      val compat = lookup_compat_thm j i cts
+    in
+      compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
+      |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
+      |> fold Thm.elim_implies agsj
+      |> fold Thm.elim_implies agsi
+      |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
     end
-
-
-
+    else
+    let
+      val compat = lookup_compat_thm i j cts
+    in
+      compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
+      |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
+      |> fold Thm.elim_implies agsi
+      |> fold Thm.elim_implies agsj
+      |> Thm.elim_implies (assume lhsi_eq_lhsj)
+      |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
+    end
+  end
 
 (* Generates the replacement lemma in fully quantified form. *)
 fun mk_replacement_lemma thy h ih_elim clause =
-    let
-        val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
-        local open Conv in
-        val ih_conv = arg1_conv o arg_conv o arg_conv
-        end
+  let
+    val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...},
+      RCs, tree, ...} = clause
+    local open Conv in
+      val ih_conv = arg1_conv o arg_conv o arg_conv
+    end
 
-        val ih_elim_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
-
-        val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
-        val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
+    val ih_elim_case =
+      Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
 
-        val (eql, _) = Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
+    val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
+    val h_assums = map (fn RCInfo {h_assum, ...} =>
+      assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
+
+    val (eql, _) =
+      Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
 
-        val replace_lemma = (eql RS meta_eq_to_obj_eq)
-                                |> implies_intr (cprop_of case_hyp)
-                                |> fold_rev (implies_intr o cprop_of) h_assums
-                                |> fold_rev (implies_intr o cprop_of) ags
-                                |> fold_rev forall_intr cqs
-                                |> Thm.close_derivation
-    in
-      replace_lemma
-    end
+    val replace_lemma = (eql RS meta_eq_to_obj_eq)
+      |> implies_intr (cprop_of case_hyp)
+      |> fold_rev (implies_intr o cprop_of) h_assums
+      |> fold_rev (implies_intr o cprop_of) ags
+      |> fold_rev forall_intr cqs
+      |> Thm.close_derivation
+  in
+    replace_lemma
+  end
 
 
 fun mk_uniqueness_clause thy globals compat_store clausei clausej RLj =
-    let
-        val Globals {h, y, x, fvar, ...} = globals
-        val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
-        val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
+  let
+    val Globals {h, y, x, fvar, ...} = globals
+    val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
+    val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
+
+    val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} =
+      mk_clause_context x ctxti cdescj
 
-        val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
-            = mk_clause_context x ctxti cdescj
+    val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
+    val compat = get_compat_thm thy compat_store i j cctxi cctxj
+    val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
 
-        val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
-        val compat = get_compat_thm thy compat_store i j cctxi cctxj
-        val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
+    val RLj_import = RLj
+      |> fold forall_elim cqsj'
+      |> fold Thm.elim_implies agsj'
+      |> fold Thm.elim_implies Ghsj'
 
-        val RLj_import =
-            RLj |> fold forall_elim cqsj'
-                |> fold Thm.elim_implies agsj'
-                |> fold Thm.elim_implies Ghsj'
-
-        val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
-        val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
-    in
-        (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
-        |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
-        |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
-        |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
-        |> fold_rev (implies_intr o cprop_of) Ghsj'
-        |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
-        |> implies_intr (cprop_of y_eq_rhsj'h)
-        |> implies_intr (cprop_of lhsi_eq_lhsj')
-        |> fold_rev forall_intr (cterm_of thy h :: cqsj')
-    end
+    val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
+    val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
+       (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
+  in
+    (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
+    |> implies_elim RLj_import
+      (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
+    |> (fn it => trans OF [it, compat])
+      (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
+    |> (fn it => trans OF [y_eq_rhsj'h, it])
+      (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
+    |> fold_rev (implies_intr o cprop_of) Ghsj'
+    |> fold_rev (implies_intr o cprop_of) agsj'
+      (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
+    |> implies_intr (cprop_of y_eq_rhsj'h)
+    |> implies_intr (cprop_of lhsi_eq_lhsj')
+    |> fold_rev forall_intr (cterm_of thy h :: cqsj')
+  end
 
 
 
 fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
-    let
-        val Globals {x, y, ranT, fvar, ...} = globals
-        val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
-        val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
+  let
+    val Globals {x, y, ranT, fvar, ...} = globals
+    val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
+    val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
 
-        val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
+    val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
 
-        fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
-                                                            |> fold_rev (implies_intr o cprop_of) CCas
-                                                            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+    fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
+      |> fold_rev (implies_intr o cprop_of) CCas
+      |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+
+    val existence = fold (curry op COMP o prep_RC) RCs lGI
 
-        val existence = fold (curry op COMP o prep_RC) RCs lGI
+    val P = cterm_of thy (mk_eq (y, rhsC))
+    val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
 
-        val P = cterm_of thy (mk_eq (y, rhsC))
-        val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
-
-        val unique_clauses = map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
+    val unique_clauses =
+      map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
 
-        val uniqueness = G_cases
-                           |> forall_elim (cterm_of thy lhs)
-                           |> forall_elim (cterm_of thy y)
-                           |> forall_elim P
-                           |> Thm.elim_implies G_lhs_y
-                           |> fold Thm.elim_implies unique_clauses
-                           |> implies_intr (cprop_of G_lhs_y)
-                           |> forall_intr (cterm_of thy y)
+    val uniqueness = G_cases
+      |> forall_elim (cterm_of thy lhs)
+      |> forall_elim (cterm_of thy y)
+      |> forall_elim P
+      |> Thm.elim_implies G_lhs_y
+      |> fold Thm.elim_implies unique_clauses
+      |> implies_intr (cprop_of G_lhs_y)
+      |> forall_intr (cterm_of thy y)
 
-        val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
+    val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
 
-        val exactly_one =
-            ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
-                 |> curry (op COMP) existence
-                 |> curry (op COMP) uniqueness
-                 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
-                 |> implies_intr (cprop_of case_hyp)
-                 |> fold_rev (implies_intr o cprop_of) ags
-                 |> fold_rev forall_intr cqs
+    val exactly_one =
+      ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
+      |> curry (op COMP) existence
+      |> curry (op COMP) uniqueness
+      |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
+      |> implies_intr (cprop_of case_hyp)
+      |> fold_rev (implies_intr o cprop_of) ags
+      |> fold_rev forall_intr cqs
 
-        val function_value =
-            existence
-              |> implies_intr ihyp
-              |> implies_intr (cprop_of case_hyp)
-              |> forall_intr (cterm_of thy x)
-              |> forall_elim (cterm_of thy lhs)
-              |> curry (op RS) refl
-    in
-        (exactly_one, function_value)
-    end
-
-
+    val function_value =
+      existence
+      |> implies_intr ihyp
+      |> implies_intr (cprop_of case_hyp)
+      |> forall_intr (cterm_of thy x)
+      |> forall_elim (cterm_of thy lhs)
+      |> curry (op RS) refl
+  in
+    (exactly_one, function_value)
+  end
 
 
 fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
-    let
-        val Globals {h, domT, ranT, x, ...} = globals
-        val thy = ProofContext.theory_of ctxt
+  let
+    val Globals {h, domT, ranT, x, ...} = globals
+    val thy = ProofContext.theory_of ctxt
 
-        (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
-        val ihyp = Term.all domT $ Abs ("z", domT,
-                                   Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
-                                     HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
-                                                             Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
-                       |> cterm_of thy
+    (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
+    val ihyp = Term.all domT $ Abs ("z", domT,
+      Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
+        HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
+          Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
+      |> cterm_of thy
 
-        val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0
-        val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
-        val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
-                        |> instantiate' [] [NONE, SOME (cterm_of thy h)]
+    val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0
+    val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
+    val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
+      |> instantiate' [] [NONE, SOME (cterm_of thy h)]
 
-        val _ = trace_msg (K "Proving Replacement lemmas...")
-        val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
+    val _ = trace_msg (K "Proving Replacement lemmas...")
+    val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
 
-        val _ = trace_msg (K "Proving cases for unique existence...")
-        val (ex1s, values) =
-            split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
+    val _ = trace_msg (K "Proving cases for unique existence...")
+    val (ex1s, values) =
+      split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
 
-        val _ = trace_msg (K "Proving: Graph is a function")
-        val graph_is_function = complete
-                                  |> Thm.forall_elim_vars 0
-                                  |> fold (curry op COMP) ex1s
-                                  |> implies_intr (ihyp)
-                                  |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
-                                  |> forall_intr (cterm_of thy x)
-                                  |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
-                                  |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
+    val _ = trace_msg (K "Proving: Graph is a function")
+    val graph_is_function = complete
+      |> Thm.forall_elim_vars 0
+      |> fold (curry op COMP) ex1s
+      |> implies_intr (ihyp)
+      |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
+      |> forall_intr (cterm_of thy x)
+      |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
+      |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
 
-        val goalstate =  Conjunction.intr graph_is_function complete
-                          |> Thm.close_derivation
-                          |> Goal.protect
-                          |> fold_rev (implies_intr o cprop_of) compat
-                          |> implies_intr (cprop_of complete)
-    in
-      (goalstate, values)
-    end
+    val goalstate =  Conjunction.intr graph_is_function complete
+      |> Thm.close_derivation
+      |> Goal.protect
+      |> fold_rev (implies_intr o cprop_of) compat
+      |> implies_intr (cprop_of complete)
+  in
+    (goalstate, values)
+  end
 
 (* wrapper -- restores quantifiers in rule specifications *)
 fun inductive_def (binding as ((R, T), _)) intrs lthy =
@@ -483,7 +458,7 @@
           forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
       end
   in
-      ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
+    ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
   end
 
 fun define_graph Gname fvar domT ranT clauses RCss lthy =
@@ -544,33 +519,30 @@
 
 
 fun fix_globals domT ranT fvar ctxt =
-    let
-      val ([h, y, x, z, a, D, P, Pbool],ctxt') =
-          Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
-    in
-      (Globals {h = Free (h, domT --> ranT),
-                y = Free (y, ranT),
-                x = Free (x, domT),
-                z = Free (z, domT),
-                a = Free (a, domT),
-                D = Free (D, domT --> boolT),
-                P = Free (P, domT --> boolT),
-                Pbool = Free (Pbool, boolT),
-                fvar = fvar,
-                domT = domT,
-                ranT = ranT
-               },
-       ctxt')
-    end
-
-
+  let
+    val ([h, y, x, z, a, D, P, Pbool],ctxt') = Variable.variant_fixes
+      ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
+  in
+    (Globals {h = Free (h, domT --> ranT),
+      y = Free (y, ranT),
+      x = Free (x, domT),
+      z = Free (z, domT),
+      a = Free (a, domT),
+      D = Free (D, domT --> boolT),
+      P = Free (P, domT --> boolT),
+      Pbool = Free (Pbool, boolT),
+      fvar = fvar,
+      domT = domT,
+      ranT = ranT},
+    ctxt')
+  end
 
 fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
-    let
-      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
+  let
+    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
 
 
 
@@ -579,27 +551,27 @@
  **********************************************************)
 
 fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
-    let
-      val Globals {domT, z, ...} = globals
+  let
+    val Globals {domT, z, ...} = globals
 
-      fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
-          let
-            val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
-            val z_smaller = cterm_of thy (HOLogic.mk_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)
-          end
-    in
-      map2 mk_psimp clauses valthms
-    end
+    fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
+      let
+        val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
+        val z_smaller = cterm_of thy (HOLogic.mk_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)
+      end
+  in
+    map2 mk_psimp clauses valthms
+  end
 
 
 (** Induction rule **)
@@ -609,232 +581,236 @@
 
 
 fun mk_partial_induct_rule thy globals R complete_thm clauses =
-    let
-      val Globals {domT, x, z, a, P, D, ...} = globals
-      val acc_R = mk_acc domT R
+  let
+    val Globals {domT, x, z, a, P, D, ...} = globals
+    val acc_R = mk_acc domT R
 
-      val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
-      val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
+    val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
+    val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
 
-      val D_subset = cterm_of thy (Logic.all x
-        (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
+    val D_subset = cterm_of thy (Logic.all x
+      (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
 
-      val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
-                    Logic.all x
-                    (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
-                                                    Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
-                                                                      HOLogic.mk_Trueprop (D $ z)))))
-                    |> cterm_of thy
-
+    val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
+      Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
+        Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
+          HOLogic.mk_Trueprop (D $ z)))))
+      |> cterm_of thy
 
-  (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
-      val ihyp = Term.all domT $ Abs ("z", domT,
-               Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
-                 HOLogic.mk_Trueprop (P $ Bound 0)))
-           |> cterm_of thy
+    (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
+    val ihyp = Term.all domT $ Abs ("z", domT,
+      Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
+        HOLogic.mk_Trueprop (P $ Bound 0)))
+      |> cterm_of thy
 
-      val aihyp = assume ihyp
+    val aihyp = assume ihyp
 
-  fun prove_case clause =
+    fun prove_case clause =
       let
-    val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
-                    qglr = (oqs, _, _, _), ...} = clause
+        val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...},
+          RCs, qglr = (oqs, _, _, _), ...} = clause
 
-    val case_hyp_conv = K (case_hyp RS eq_reflection)
-    local open Conv in
-    val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
-    val sih = fconv_rule (More_Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
-    end
+        val case_hyp_conv = K (case_hyp RS eq_reflection)
+        local open Conv in
+          val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
+          val sih =
+            fconv_rule (More_Conv.binder_conv
+              (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
+        end
 
-    fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
-        sih |> forall_elim (cterm_of thy rcarg)
-            |> Thm.elim_implies llRI
-            |> fold_rev (implies_intr o cprop_of) CCas
-            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+        fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
+          |> forall_elim (cterm_of thy rcarg)
+          |> Thm.elim_implies 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 P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
 
-    val step = HOLogic.mk_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 (HOLogic.mk_Trueprop (D $ lhs))
-            |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
-            |> cterm_of thy
+        val step = HOLogic.mk_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 (HOLogic.mk_Trueprop (D $ lhs))
+          |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+          |> cterm_of thy
 
-    val P_lhs = assume step
-           |> fold forall_elim cqs
-           |> Thm.elim_implies lhs_D
-           |> fold Thm.elim_implies ags
-           |> fold Thm.elim_implies P_recs
+        val P_lhs = assume step
+          |> fold forall_elim cqs
+          |> Thm.elim_implies lhs_D
+          |> fold Thm.elim_implies ags
+          |> fold Thm.elim_implies P_recs
 
-    val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
-           |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
-           |> 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
+        val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
+          |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
+          |> 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)
+    val (cases, steps) = split_list (map prove_case clauses)
 
-  val istep = complete_thm
-                |> 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 istep = complete_thm
+      |> 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 =
+    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
+      |> (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 =
+    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
-      simple_induct_rule
-    end
+      |> 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
+    simple_induct_rule
+  end
 
 
-
-(* FIXME: This should probably use fixed goals, to be more reliable and faster *)
+(* FIXME: broken by design *)
 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
-    let
-      val thy = ProofContext.theory_of ctxt
-      val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
-                      qglr = (oqs, _, _, _), ...} = clause
-      val goal = HOLogic.mk_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 [Thm.forall_elim_vars 0 R_cases] 1))  |> the
-      |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
-      |> Goal.conclude
-      |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
-    end
+  let
+    val thy = ProofContext.theory_of ctxt
+    val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
+      qglr = (oqs, _, _, _), ...} = clause
+    val goal = HOLogic.mk_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 [Thm.forall_elim_vars 0 R_cases] 1))  |> the
+    |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
+    |> Goal.conclude
+    |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
+  end
 
 
 
 (** Termination rule **)
 
-val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule};
-val wf_in_rel = @{thm FunDef.wf_in_rel};
-val in_rel_def = @{thm FunDef.in_rel_def};
+val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}
+val wf_in_rel = @{thm FunDef.wf_in_rel}
+val in_rel_def = @{thm FunDef.in_rel_def}
 
 fun mk_nest_term_case thy globals R' ihyp clause =
-    let
-      val Globals {z, ...} = globals
-      val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...},tree,
-                      qglr=(oqs, _, _, _), ...} = clause
+  let
+    val Globals {z, ...} = globals
+    val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree,
+      qglr=(oqs, _, _, _), ...} = clause
 
-      val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
+    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 (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) (u @ sub)
+    fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
+      let
+        val used = (u @ sub)
+          |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm)
 
-            val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
-                      |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
-                      |> Function_Ctx_Tree.export_term (fixes, assumes)
-                      |> fold_rev (curry Logic.mk_implies o prop_of) ags
-                      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
-                      |> cterm_of thy
+        val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
+          |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
+          |> Function_Ctx_Tree.export_term (fixes, 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 Thm.elim_implies ags
-                      |> Function_Ctx_Tree.import_thm thy (fixes, assumes)
-                      |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
+        val thm = assume hyp
+          |> fold forall_elim cqs
+          |> fold Thm.elim_implies ags
+          |> Function_Ctx_Tree.import_thm thy (fixes, assumes)
+          |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
 
-            val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
+        val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg))
+          |> cterm_of thy |> assume
 
-            val acc = thm COMP ih_case
-            val z_acc_local = acc
-            |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
+        val acc = thm COMP ih_case
+        val z_acc_local = acc
+          |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
 
-            val ethm = z_acc_local
-                         |> Function_Ctx_Tree.export_thm thy (fixes,
-                                                          z_eq_arg :: case_hyp :: ags @ assumes)
-                         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
+        val ethm = z_acc_local
+          |> Function_Ctx_Tree.export_thm thy (fixes,
+               z_eq_arg :: case_hyp :: 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
-    in
-      Function_Ctx_Tree.traverse_tree step tree
-    end
+        val sub' = sub @ [(([],[]), acc)]
+      in
+        (sub', (hyp :: hyps, ethm :: thms))
+      end
+      | step _ _ _ _ = raise Match
+  in
+    Function_Ctx_Tree.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
+  let
+    val Globals { domT, x, z, ... } = globals
+    val acc_R = mk_acc domT R
 
-      val R' = Free ("R", fastype_of R)
+    val R' = Free ("R", fastype_of R)
 
-      val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
-      val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
+    val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
+    val inrel_R = Const (@{const_name FunDef.in_rel},
+      HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
 
-      val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
+    val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},
+      (domT --> domT --> boolT) --> boolT) $ R')
+      |> cterm_of thy (* "wf R'" *)
 
-      (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
-      val ihyp = Term.all domT $ Abs ("z", domT,
-                                 Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
-                                   HOLogic.mk_Trueprop (acc_R $ Bound 0)))
-                     |> cterm_of thy
+    (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
+    val ihyp = Term.all domT $ Abs ("z", domT,
+      Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
+        HOLogic.mk_Trueprop (acc_R $ Bound 0)))
+      |> cterm_of thy
 
-      val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
+    val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
 
-      val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
+    val R_z_x = cterm_of thy (HOLogic.mk_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')
-        |> forall_intr_vars
-        |> (fn it => it COMP allI)
-        |> 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
+    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')
+    |> forall_intr_vars
+    |> (fn it => it COMP allI)
+    |> 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
 
 
 
@@ -846,135 +822,150 @@
  * - Splitting is not configured automatically: Problems with case?
  *)
 fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
-    let
-      val Globals {domT, ranT, fvar, ...} = globals
+  let
+    val Globals {domT, ranT, fvar, ...} = globals
 
-      val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
+    val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
 
-      val graph_implies_dom = (* "G ?x ?y ==> dom ?x"  *)
-          Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
-                     (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
-                     (fn {prems=[a], ...} =>
-                         ((rtac (G_induct OF [a]))
-                            THEN_ALL_NEW (rtac accI)
-                            THEN_ALL_NEW (etac R_cases)
-                            THEN_ALL_NEW (asm_full_simp_tac (simpset_of octxt))) 1)
+    val graph_implies_dom = (* "G ?x ?y ==> dom ?x"  *)
+      Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
+        (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
+        (fn {prems=[a], ...} =>
+          ((rtac (G_induct OF [a]))
+          THEN_ALL_NEW rtac accI
+          THEN_ALL_NEW etac R_cases
+          THEN_ALL_NEW asm_full_simp_tac (simpset_of octxt)) 1)
 
-      val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
+    val default_thm =
+      forall_intr_vars graph_implies_dom COMP (f_def COMP fundef_default_value)
 
-      fun mk_trsimp clause psimp =
-          let
-            val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause
-            val thy = ProofContext.theory_of ctxt
-            val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
+    fun mk_trsimp clause psimp =
+      let
+        val ClauseInfo {qglr = (oqs, _, _, _), cdata =
+          ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause
+        val thy = ProofContext.theory_of ctxt
+        val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
 
-            val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
-            val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
-            fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def])
-          in
-            Goal.prove ctxt [] [] trsimp
-                       (fn _ =>
-                           rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
-                                THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
-                                THEN (simp_default_tac (simpset_of ctxt) 1)
-                                THEN (etac not_acc_down 1)
-                                THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)
-              |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
-          end
-    in
-      map2 mk_trsimp clauses psimps
-    end
+        val trsimp = Logic.list_implies(gs,
+          HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
+        val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
+        fun simp_default_tac ss =
+          asm_full_simp_tac (ss addsimps [default_thm, Let_def])
+      in
+        Goal.prove ctxt [] [] trsimp (fn _ =>
+          rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
+          THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
+          THEN (simp_default_tac (simpset_of ctxt) 1)
+          THEN (etac not_acc_down 1)
+          THEN ((etac R_cases)
+            THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)
+        |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
+      end
+  in
+    map2 mk_trsimp clauses psimps
+  end
 
 
 fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
-    let
-      val FunctionConfig {domintros, tailrec, default=default_str, ...} = config
+  let
+    val FunctionConfig {domintros, tailrec, default=default_str, ...} = config
 
-      val fvar = Free (fname, fT)
-      val domT = domain_type fT
-      val ranT = range_type fT
+    val fvar = Free (fname, fT)
+    val domT = domain_type fT
+    val ranT = range_type fT
 
-      val default = Syntax.parse_term lthy default_str
-        |> TypeInfer.constrain fT |> Syntax.check_term lthy
+    val default = Syntax.parse_term lthy default_str
+      |> TypeInfer.constrain fT |> Syntax.check_term lthy
+
+    val (globals, ctxt') = fix_globals domT ranT fvar lthy
 
-      val (globals, ctxt') = fix_globals domT ranT fvar lthy
+    val Globals { x, h, ... } = globals
 
-      val Globals { x, h, ... } = globals
+    val clauses = map (mk_clause_context x ctxt') abstract_qglrs
+
+    val n = length abstract_qglrs
 
-      val clauses = map (mk_clause_context x ctxt') abstract_qglrs
+    fun build_tree (ClauseContext { ctxt, rhs, ...}) =
+       Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
 
-      val n = length abstract_qglrs
-
-      fun build_tree (ClauseContext { ctxt, rhs, ...}) =
-            Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
+    val trees = map build_tree clauses
+    val RCss = map find_calls trees
 
-      val trees = map build_tree clauses
-      val RCss = map find_calls trees
+    val ((G, GIntro_thms, G_elim, G_induct), lthy) =
+      PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
+
+    val ((f, (_, f_defthm)), lthy) =
+      PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
 
-      val ((G, GIntro_thms, G_elim, G_induct), lthy) =
-          PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
+    val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
+    val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
 
-      val ((f, (_, f_defthm)), lthy) =
-          PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
+    val ((R, RIntro_thmss, R_elim), lthy) =
+      PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
 
-      val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
-      val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
+    val (_, lthy) =
+      Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
 
-      val ((R, RIntro_thmss, R_elim), lthy) =
-          PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
+    val newthy = ProofContext.theory_of lthy
+    val clauses = map (transfer_clause_ctx newthy) clauses
 
-      val (_, lthy) =
-          Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
+    val cert = cterm_of (ProofContext.theory_of lthy)
 
-      val newthy = ProofContext.theory_of lthy
-      val clauses = map (transfer_clause_ctx newthy) clauses
-
-      val cert = cterm_of (ProofContext.theory_of lthy)
+    val xclauses = PROFILE "xclauses"
+      (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
+        RCss GIntro_thms) RIntro_thmss
 
-      val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
-
-      val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
-      val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
+    val complete =
+      mk_completeness globals clauses abstract_qglrs |> cert |> assume
 
-      val compat_store = store_compat_thms n compat
+    val compat =
+      mk_compat_proof_obligations domT ranT fvar f abstract_qglrs
+      |> map (cert #> assume)
 
-      val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim) f_defthm
-
-      val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
+    val compat_store = store_compat_thms n compat
 
-      fun mk_partial_rules provedgoal =
-          let
-            val newthy = theory_of_thm provedgoal (*FIXME*)
+    val (goalstate, values) = PROFILE "prove_stuff"
+      (prove_stuff lthy globals G f R xclauses complete compat
+         compat_store G_elim) f_defthm
+
+    val mk_trsimps =
+      mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
 
-            val (graph_is_function, complete_thm) =
-                provedgoal
-                  |> Conjunction.elim
-                  |> apfst (Thm.forall_elim_vars 0)
+    fun mk_partial_rules provedgoal =
+      let
+        val newthy = theory_of_thm provedgoal (*FIXME*)
 
-            val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
+        val (graph_is_function, complete_thm) =
+          provedgoal
+          |> Conjunction.elim
+          |> apfst (Thm.forall_elim_vars 0)
 
-            val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
+        val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
+
+        val psimps = PROFILE "Proving simplification rules"
+          (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
 
-            val simple_pinduct = PROFILE "Proving partial induction rule"
-                                                           (mk_partial_induct_rule newthy globals R complete_thm) xclauses
+        val simple_pinduct = PROFILE "Proving partial induction rule"
+          (mk_partial_induct_rule newthy globals R complete_thm) xclauses
 
-
-            val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
+        val total_intro = PROFILE "Proving nested termination rule"
+          (mk_nest_term_rule newthy globals R R_elim) xclauses
 
-            val dom_intros = if domintros
-                             then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses)
-                             else NONE
-            val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
+        val dom_intros =
+          if domintros then SOME (PROFILE "Proving domain introduction rules"
+             (map (mk_domain_intro lthy globals R R_elim)) xclauses)
+           else NONE
+        val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
 
-          in
-            FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
-                          psimps=psimps, simple_pinducts=[simple_pinduct],
-                          termination=total_intro, trsimps=trsimps,
-                          domintros=dom_intros}
-          end
-    in
-      ((f, goalstate, mk_partial_rules), lthy)
-    end
+      in
+        FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
+          psimps=psimps, simple_pinducts=[simple_pinduct],
+          termination=total_intro, trsimps=trsimps,
+          domintros=dom_intros}
+      end
+  in
+    ((f, goalstate, mk_partial_rules), lthy)
+  end
 
 
 end
--- a/src/HOL/Tools/Function/function_lib.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -1,14 +1,14 @@
 (*  Title:      HOL/Tools/Function/fundef_lib.ML
     Author:     Alexander Krauss, TU Muenchen
 
-A package for general recursive function definitions. 
-Some fairly general functions that should probably go somewhere else... 
+A package for general recursive function definitions.
+Some fairly general functions that should probably go somewhere else...
 *)
 
 structure Function_Lib =
 struct
 
-fun map_option f NONE = NONE 
+fun map_option f NONE = NONE
   | map_option f (SOME x) = SOME (f x);
 
 fun fold_option f NONE y = y
@@ -21,50 +21,50 @@
 (* lambda-abstracts over an arbitrarily nested tuple
   ==> hologic.ML? *)
 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 =>  
+  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
+  | _ => raise Match
 
 
 fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
-    let
-      val (n, body) = Term.dest_abs a
-    in
-      (Free (n, T), body)
-    end
+  let
+    val (n, body) = Term.dest_abs a
+  in
+    (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",_) $ _)) = 
-    let
-      val (v,b) = dest_all t
-      val (vs, b') = dest_all_all b
-    in
-      (v :: vs, b')
-    end
+fun dest_all_all (t as (Const ("all",_) $ _)) =
+  let
+    val (v,b) = dest_all t
+    val (vs, b') = dest_all_all b
+  in
+    (v :: vs, b')
+  end
   | dest_all_all t = ([],t)
 
 
 (* FIXME: similar to Variable.focus *)
 fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (n,T,b)) =
-    let
-      val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
-      val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
+  let
+    val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
+    val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
 
-      val (n'', body) = Term.dest_abs (n', T, b) 
-      val _ = (n' = n'') orelse error "dest_all_ctx"
+    val (n'', body) = Term.dest_abs (n', T, b)
+    val _ = (n' = n'') orelse error "dest_all_ctx"
       (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *)
 
-      val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
-    in
-      (ctx'', (n', T) :: vs, bd)
-    end
-  | dest_all_all_ctx ctx t = 
-    (ctx, [], t)
+    val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
+  in
+    (ctx'', (n', T) :: vs, bd)
+  end
+  | dest_all_all_ctx ctx t =
+  (ctx, [], t)
 
 
 fun map3 _ [] [] [] = []
@@ -86,52 +86,51 @@
 
 
 (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
-(* ==> library *)
 fun unordered_pairs [] = []
   | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
 
 
 (* Replaces Frees by name. Works with loose Bounds. *)
 fun replace_frees assoc =
-    map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
-                 | t => t)
+  map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
+    | t => t)
 
 
-fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b))
+fun rename_bound n (Q $ Abs (_, T, b)) = (Q $ Abs (n, T, b))
   | rename_bound n _ = raise Match
 
 fun mk_forall_rename (n, v) =
-    rename_bound n o Logic.all v 
+  rename_bound n o Logic.all v
 
 fun forall_intr_rename (n, cv) thm =
-    let
-      val allthm = forall_intr cv thm
-      val (_ $ abs) = prop_of allthm
-    in
-      Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm
-    end
+  let
+    val allthm = forall_intr cv thm
+    val (_ $ abs) = prop_of allthm
+  in
+    Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm
+  end
 
 
 (* Returns the frees in a term in canonical order, excluding the fixes from the context *)
 fun frees_in_term ctxt t =
-    Term.add_frees t []
-    |> filter_out (Variable.is_fixed ctxt o fst)
-    |> rev
+  Term.add_frees t []
+  |> filter_out (Variable.is_fixed ctxt o fst)
+  |> rev
 
 
 datatype proof_attempt = Solved of thm | Stuck of thm | Fail
 
-fun try_proof cgoal tac = 
-    case SINGLE tac (Goal.init cgoal) of
-      NONE => Fail
-    | SOME st =>
-        if Thm.no_prems st
-        then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st)
-        else Stuck st
+fun try_proof cgoal tac =
+  case SINGLE tac (Goal.init cgoal) of
+    NONE => Fail
+  | SOME st =>
+    if Thm.no_prems st
+    then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st)
+    else Stuck st
 
 
-fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = 
-    if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ]
+fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) =
+  if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ]
   | dest_binop_list _ t = [ t ]
 
 
@@ -168,10 +167,10 @@
  end
 
 (* instance for unions *)
-fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
-  (map (fn t => t RS eq_reflection) (@{thms Un_ac} @
-                                     @{thms Un_empty_right} @
-                                     @{thms Un_empty_left})) t
+val regroup_union_conv =
+  regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
+    (map (fn t => t RS eq_reflection)
+      (@{thms Un_ac} @ @{thms Un_empty_right} @ @{thms Un_empty_left}))
 
 
 end
--- a/src/HOL/Tools/Function/induction_schema.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -18,370 +18,367 @@
 
 open Function_Lib
 
-
 type rec_call_info = int * (string * typ) list * term list * term list
 
-datatype scheme_case =
-  SchemeCase of
-  {
-   bidx : int,
-   qs: (string * typ) list,
-   oqnames: string list,
-   gs: term list,
-   lhs: term list,
-   rs: rec_call_info list
-  }
+datatype scheme_case = SchemeCase of
+ {bidx : int,
+  qs: (string * typ) list,
+  oqnames: string list,
+  gs: term list,
+  lhs: term list,
+  rs: rec_call_info list}
 
-datatype scheme_branch = 
-  SchemeBranch of
-  {
-   P : term,
-   xs: (string * typ) list,
-   ws: (string * typ) list,
-   Cs: term list
-  }
+datatype scheme_branch = SchemeBranch of
+ {P : term,
+  xs: (string * typ) list,
+  ws: (string * typ) list,
+  Cs: term list}
 
-datatype ind_scheme =
-  IndScheme of
-  {
-   T: typ, (* sum of products *)
-   branches: scheme_branch list,
-   cases: scheme_case list
-  }
+datatype ind_scheme = IndScheme of
+ {T: typ, (* sum of products *)
+  branches: scheme_branch list,
+  cases: scheme_case list}
 
 val ind_atomize = MetaSimplifier.rewrite true @{thms induct_atomize}
 val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify}
 
 fun meta thm = thm RS eq_reflection
 
-val sum_prod_conv = MetaSimplifier.rewrite true 
-                    (map meta (@{thm split_conv} :: @{thms sum.cases}))
+val sum_prod_conv = MetaSimplifier.rewrite true
+  (map meta (@{thm split_conv} :: @{thms sum.cases}))
 
-fun term_conv thy cv t = 
-    cv (cterm_of thy t)
-    |> prop_of |> Logic.dest_equals |> snd
+fun term_conv thy cv t =
+  cv (cterm_of thy t)
+  |> prop_of |> Logic.dest_equals |> snd
 
 fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T))
 
-fun dest_hhf ctxt t = 
-    let 
-      val (ctxt', vars, imp) = dest_all_all_ctx ctxt t
-    in
-      (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
-    end
-
+fun dest_hhf ctxt t =
+  let
+    val (ctxt', vars, imp) = dest_all_all_ctx ctxt t
+  in
+    (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
+  end
 
 fun mk_scheme' ctxt cases concl =
-    let
-      fun mk_branch concl =
+  let
+    fun mk_branch concl =
+      let
+        val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
+        val (P, xs) = strip_comb Pxs
+      in
+        SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
+      end
+
+    val (branches, cases') = (* correction *)
+      case Logic.dest_conjunction_list concl of
+        [conc] =>
+        let
+          val _ $ Pxs = Logic.strip_assums_concl conc
+          val (P, _) = strip_comb Pxs
+          val (cases', conds) =
+            take_prefix (Term.exists_subterm (curry op aconv P)) cases
+          val concl' = fold_rev (curry Logic.mk_implies) conds conc
+        in
+          ([mk_branch concl'], cases')
+        end
+      | concls => (map mk_branch concls, cases)
+
+    fun mk_case premise =
+      let
+        val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise
+        val (P, lhs) = strip_comb Plhs
+
+        fun bidx Q =
+          find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches
+
+        fun mk_rcinfo pr =
           let
-            val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
-            val (P, xs) = strip_comb Pxs
+            val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
+            val (P', rcs) = strip_comb Phyp
           in
-            SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
+            (bidx P', Gvs, Gas, rcs)
           end
 
-      val (branches, cases') = (* correction *)
-          case Logic.dest_conjunction_list concl of
-            [conc] => 
-            let 
-              val _ $ Pxs = Logic.strip_assums_concl conc
-              val (P, _) = strip_comb Pxs
-              val (cases', conds) = take_prefix (Term.exists_subterm (curry op aconv P)) cases
-              val concl' = fold_rev (curry Logic.mk_implies) conds conc
-            in
-              ([mk_branch concl'], cases')
-            end
-          | concls => (map mk_branch concls, cases)
-
-      fun mk_case premise =
-          let
-            val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise
-            val (P, lhs) = strip_comb Plhs
-                                
-            fun bidx Q = find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches
+        fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches
 
-            fun mk_rcinfo pr =
-                let
-                  val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
-                  val (P', rcs) = strip_comb Phyp
-                in
-                  (bidx P', Gvs, Gas, rcs)
-                end
-                
-            fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches
+        val (gs, rcprs) =
+          take_prefix (not o Term.exists_subterm is_pred) prems
+      in
+        SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*),
+          gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs}
+      end
 
-            val (gs, rcprs) = 
-                take_prefix (not o Term.exists_subterm is_pred) prems
-          in
-            SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*), gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs}
-          end
+    fun PT_of (SchemeBranch { xs, ...}) =
+      foldr1 HOLogic.mk_prodT (map snd xs)
 
-      fun PT_of (SchemeBranch { xs, ...}) =
-            foldr1 HOLogic.mk_prodT (map snd xs)
-
-      val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
-    in
-      IndScheme {T=ST, cases=map mk_case cases', branches=branches }
-    end
-
-
+    val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
+  in
+    IndScheme {T=ST, cases=map mk_case cases', branches=branches }
+  end
 
 fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx =
-    let
-      val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx
-      val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases
+  let
+    val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx
+    val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases
+
+    val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases []
+    val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs))
+    val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
 
-      val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases []
-      val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs))
-      val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
-                       
-      fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) =
-          HOLogic.mk_Trueprop Pbool
-                     |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l)))
-                                 (xs' ~~ lhs)
-                     |> fold_rev (curry Logic.mk_implies) gs
-                     |> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
-    in
+    fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) =
       HOLogic.mk_Trueprop Pbool
-       |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases
-       |> fold_rev (curry Logic.mk_implies) Cs'
-       |> fold_rev (Logic.all o Free) ws
-       |> fold_rev mk_forall_rename (map fst xs ~~ xs')
-       |> mk_forall_rename ("P", Pbool)
-    end
+      |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l)))
+           (xs' ~~ lhs)
+      |> fold_rev (curry Logic.mk_implies) gs
+      |> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
+  in
+    HOLogic.mk_Trueprop Pbool
+    |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases
+    |> fold_rev (curry Logic.mk_implies) Cs'
+    |> fold_rev (Logic.all o Free) ws
+    |> fold_rev mk_forall_rename (map fst xs ~~ xs')
+    |> mk_forall_rename ("P", Pbool)
+  end
 
 fun mk_wf R (IndScheme {T, ...}) =
-    HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
+  HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
 
 fun mk_ineqs R (IndScheme {T, cases, branches}) =
-    let
-      fun inject i ts =
-          SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
+  let
+    fun inject i ts =
+       SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
 
-      val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *)
+    val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *)
 
-      fun mk_pres bdx args = 
-          let
-            val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx
-            fun replace (x, v) t = betapply (lambda (Free x) t, v)
-            val Cs' = map (fold replace (xs ~~ args)) Cs
-            val cse = 
-                HOLogic.mk_Trueprop thesis
-                |> fold_rev (curry Logic.mk_implies) Cs'
-                |> fold_rev (Logic.all o Free) ws
-          in
-            Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis)
-          end
+    fun mk_pres bdx args =
+      let
+        val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx
+        fun replace (x, v) t = betapply (lambda (Free x) t, v)
+        val Cs' = map (fold replace (xs ~~ args)) Cs
+        val cse =
+          HOLogic.mk_Trueprop thesis
+          |> fold_rev (curry Logic.mk_implies) Cs'
+          |> fold_rev (Logic.all o Free) ws
+      in
+        Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis)
+      end
 
-      fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) = 
-          let
-            fun g (bidx', Gvs, Gas, rcarg) =
-                let val export = 
-                         fold_rev (curry Logic.mk_implies) Gas
-                         #> fold_rev (curry Logic.mk_implies) gs
-                         #> fold_rev (Logic.all o Free) Gvs
-                         #> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
-                in
-                (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R)
-                 |> HOLogic.mk_Trueprop
-                 |> export,
-                 mk_pres bidx' rcarg
-                 |> export
-                 |> Logic.all thesis)
-                end
+    fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) =
+      let
+        fun g (bidx', Gvs, Gas, rcarg) =
+          let val export =
+            fold_rev (curry Logic.mk_implies) Gas
+            #> fold_rev (curry Logic.mk_implies) gs
+            #> fold_rev (Logic.all o Free) Gvs
+            #> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
           in
-            map g rs
+            (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R)
+             |> HOLogic.mk_Trueprop
+             |> export,
+             mk_pres bidx' rcarg
+             |> export
+             |> Logic.all thesis)
           end
-    in
-      map f cases
-    end
+      in
+        map g rs
+      end
+  in
+    map f cases
+  end
 
 
 fun mk_ind_goal thy branches =
-    let
-      fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
-          HOLogic.mk_Trueprop (list_comb (P, map Free xs))
-          |> fold_rev (curry Logic.mk_implies) Cs
-          |> fold_rev (Logic.all o Free) ws
-          |> term_conv thy ind_atomize
-          |> ObjectLogic.drop_judgment thy
-          |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
-    in
-      SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
-    end
+  let
+    fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
+      HOLogic.mk_Trueprop (list_comb (P, map Free xs))
+      |> fold_rev (curry Logic.mk_implies) Cs
+      |> fold_rev (Logic.all o Free) ws
+      |> term_conv thy ind_atomize
+      |> ObjectLogic.drop_judgment thy
+      |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
+  in
+    SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
+  end
+
+fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss
+  (IndScheme {T, cases=scases, branches}) =
+  let
+    val n = length branches
+    val scases_idx = map_index I scases
+
+    fun inject i ts =
+      SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
+    val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
+
+    val thy = ProofContext.theory_of ctxt
+    val cert = cterm_of thy
+
+    val P_comp = mk_ind_goal thy branches
+
+    (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
+    val ihyp = Term.all T $ Abs ("z", T,
+      Logic.mk_implies
+        (HOLogic.mk_Trueprop (
+          Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
+          $ (HOLogic.pair_const T T $ Bound 0 $ x)
+          $ R),
+         HOLogic.mk_Trueprop (P_comp $ Bound 0)))
+      |> cert
+
+    val aihyp = assume ihyp
+
+    (* Rule for case splitting along the sum types *)
+    val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
+    val pats = map_index (uncurry inject) xss
+    val sum_split_rule =
+      Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
+
+    fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
+      let
+        val fxs = map Free xs
+        val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
+
+        val C_hyps = map (cert #> assume) Cs
+
+        val (relevant_cases, ineqss') =
+          (scases_idx ~~ ineqss)
+          |> filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx)
+          |> split_list
+
+        fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
+          let
+            val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
+
+            val cqs = map (cert o Free) qs
+            val ags = map (assume o cert) gs
+
+            val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
+            val sih = full_simplify replace_x_ss aihyp
+
+            fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
+              let
+                val cGas = map (assume o cert) Gas
+                val cGvs = map (cert o Free) Gvs
+                val import = fold forall_elim (cqs @ cGvs)
+                  #> fold Thm.elim_implies (ags @ cGas)
+                val ipres = pres
+                  |> forall_elim (cert (list_comb (P_of idx, rcargs)))
+                  |> import
+              in
+                sih
+                |> forall_elim (cert (inject idx rcargs))
+                |> Thm.elim_implies (import ineq) (* Psum rcargs *)
+                |> Conv.fconv_rule sum_prod_conv
+                |> Conv.fconv_rule ind_rulify
+                |> (fn th => th COMP ipres) (* P rs *)
+                |> fold_rev (implies_intr o cprop_of) cGas
+                |> fold_rev forall_intr cGvs
+              end
+
+            val P_recs = map2 mk_Prec rs ineq_press   (*  [P rec1, P rec2, ... ]  *)
+
+            val step = HOLogic.mk_Trueprop (list_comb (P, lhs))
+              |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
+              |> fold_rev (curry Logic.mk_implies) gs
+              |> fold_rev (Logic.all o Free) qs
+              |> cert
+
+            val Plhs_to_Pxs_conv =
+              foldl1 (uncurry Conv.combination_conv)
+                (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps)
+
+            val res = assume step
+              |> fold forall_elim cqs
+              |> fold Thm.elim_implies ags
+              |> fold Thm.elim_implies P_recs (* P lhs *)
+              |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *)
+              |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps)
+              |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
+          in
+            (res, (cidx, step))
+          end
+
+        val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
+
+        val bstep = complete_thm
+          |> forall_elim (cert (list_comb (P, fxs)))
+          |> fold (forall_elim o cert) (fxs @ map Free ws)
+          |> fold Thm.elim_implies C_hyps
+          |> fold Thm.elim_implies cases (* P xs *)
+          |> fold_rev (implies_intr o cprop_of) C_hyps
+          |> fold_rev (forall_intr o cert o Free) ws
+
+        val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
+          |> Goal.init
+          |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
+              THEN CONVERSION ind_rulify 1)
+          |> Seq.hd
+          |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
+          |> Goal.finish ctxt
+          |> implies_intr (cprop_of branch_hyp)
+          |> fold_rev (forall_intr o cert) fxs
+      in
+        (Pxs, steps)
+      end
+
+    val (branches, steps) =
+      map_index prove_branch (branches ~~ (complete_thms ~~ pats))
+      |> split_list |> apsnd flat
+
+    val istep = sum_split_rule
+      |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
+      |> implies_intr ihyp
+      |> forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
+
+    val induct_rule =
+      @{thm "wf_induct_rule"}
+      |> (curry op COMP) wf_thm
+      |> (curry op COMP) istep
+
+    val steps_sorted = map snd (sort (int_ord o pairself fst) steps)
+  in
+    (steps_sorted, induct_rule)
+  end
 
 
-fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss (IndScheme {T, cases=scases, branches}) =
-    let
-      val n = length branches
-
-      val scases_idx = map_index I scases
-
-      fun inject i ts =
-          SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
-      val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
-
-      val thy = ProofContext.theory_of ctxt
-      val cert = cterm_of thy 
-
-      val P_comp = mk_ind_goal thy branches
-
-      (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
-      val ihyp = Term.all T $ Abs ("z", T, 
-               Logic.mk_implies
-                 (HOLogic.mk_Trueprop (
-                  Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
-                    $ (HOLogic.pair_const T T $ Bound 0 $ x) 
-                    $ R),
-                   HOLogic.mk_Trueprop (P_comp $ Bound 0)))
-           |> cert
-
-      val aihyp = assume ihyp
-
-     (* Rule for case splitting along the sum types *)
-      val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
-      val pats = map_index (uncurry inject) xss
-      val sum_split_rule = Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
-
-      fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
-          let
-            val fxs = map Free xs
-            val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
-                             
-            val C_hyps = map (cert #> assume) Cs
-
-            val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss)
-                                            |> split_list
-                           
-            fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
-                let
-                  val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
-                           
-                  val cqs = map (cert o Free) qs
-                  val ags = map (assume o cert) gs
-                            
-                  val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
-                  val sih = full_simplify replace_x_ss aihyp
-                            
-                  fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
-                      let
-                        val cGas = map (assume o cert) Gas
-                        val cGvs = map (cert o Free) Gvs
-                        val import = fold forall_elim (cqs @ cGvs)
-                                     #> fold Thm.elim_implies (ags @ cGas)
-                        val ipres = pres
-                                     |> forall_elim (cert (list_comb (P_of idx, rcargs)))
-                                     |> import
-                      in
-                        sih |> forall_elim (cert (inject idx rcargs))
-                            |> Thm.elim_implies (import ineq) (* Psum rcargs *)
-                            |> Conv.fconv_rule sum_prod_conv
-                            |> Conv.fconv_rule ind_rulify
-                            |> (fn th => th COMP ipres) (* P rs *)
-                            |> fold_rev (implies_intr o cprop_of) cGas
-                            |> fold_rev forall_intr cGvs
-                      end
-                      
-                  val P_recs = map2 mk_Prec rs ineq_press   (*  [P rec1, P rec2, ... ]  *)
-                               
-                  val step = HOLogic.mk_Trueprop (list_comb (P, lhs))
-                             |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
-                             |> fold_rev (curry Logic.mk_implies) gs
-                             |> fold_rev (Logic.all o Free) qs
-                             |> cert
-                             
-                  val Plhs_to_Pxs_conv = 
-                      foldl1 (uncurry Conv.combination_conv) 
-                      (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps)
-
-                  val res = assume step
-                                   |> fold forall_elim cqs
-                                   |> fold Thm.elim_implies ags
-                                   |> fold Thm.elim_implies P_recs (* P lhs *) 
-                                   |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *)
-                                   |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps)
-                                   |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
-                in
-                  (res, (cidx, step))
-                end
-
-            val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
-
-            val bstep = complete_thm
-                |> forall_elim (cert (list_comb (P, fxs)))
-                |> fold (forall_elim o cert) (fxs @ map Free ws)
-                |> fold Thm.elim_implies C_hyps             (* FIXME: optimization using rotate_prems *)
-                |> fold Thm.elim_implies cases (* P xs *)
-                |> fold_rev (implies_intr o cprop_of) C_hyps
-                |> fold_rev (forall_intr o cert o Free) ws
-
-            val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
-                     |> Goal.init
-                     |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
-                         THEN CONVERSION ind_rulify 1)
-                     |> Seq.hd
-                     |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
-                     |> Goal.finish ctxt
-                     |> implies_intr (cprop_of branch_hyp)
-                     |> fold_rev (forall_intr o cert) fxs
-          in
-            (Pxs, steps)
-          end
-
-      val (branches, steps) = split_list (map_index prove_branch (branches ~~ (complete_thms ~~ pats)))
-                              |> apsnd flat
-                           
-      val istep = sum_split_rule
-                |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
-                |> implies_intr ihyp
-                |> forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
-         
-      val induct_rule =
-          @{thm "wf_induct_rule"}
-            |> (curry op COMP) wf_thm 
-            |> (curry op COMP) istep
-
-      val steps_sorted = map snd (sort (int_ord o pairself fst) steps)
-    in
-      (steps_sorted, induct_rule)
-    end
-
-
-fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts = (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL 
-(SUBGOAL (fn (t, i) =>
+fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts =
+  (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) =>
   let
     val (ctxt', _, cases, concl) = dest_hhf ctxt t
     val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
-(*     val _ = tracing (makestring scheme)*)
     val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
     val R = Free (Rn, mk_relT ST)
     val x = Free (xn, ST)
     val cert = cterm_of (ProofContext.theory_of ctxt)
 
     val ineqss = mk_ineqs R scheme
-                   |> map (map (pairself (assume o cert)))
-    val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
+      |> map (map (pairself (assume o cert)))
+    val complete =
+      map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
     val wf_thm = mk_wf R scheme |> cert |> assume
 
     val (descent, pres) = split_list (flat ineqss)
-    val newgoals = complete @ pres @ wf_thm :: descent 
+    val newgoals = complete @ pres @ wf_thm :: descent
 
-    val (steps, indthm) = mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme
+    val (steps, indthm) =
+      mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme
 
     fun project (i, SchemeBranch {xs, ...}) =
-        let
-          val inst = cert (SumTree.mk_inj ST (length branches) (i + 1) (foldr1 HOLogic.mk_prod (map Free xs)))
-        in
-          indthm |> Drule.instantiate' [] [SOME inst]
-                 |> simplify SumTree.sumcase_split_ss
-                 |> Conv.fconv_rule ind_rulify
-(*                 |> (fn thm => (tracing (makestring thm); thm))*)
-        end                  
+      let
+        val inst = (foldr1 HOLogic.mk_prod (map Free xs))
+          |> SumTree.mk_inj ST (length branches) (i + 1)
+          |> cert
+      in
+        indthm
+        |> Drule.instantiate' [] [SOME inst]
+        |> simplify SumTree.sumcase_split_ss
+        |> Conv.fconv_rule ind_rulify
+      end
 
     val res = Conjunction.intr_balanced (map_index project branches)
-                 |> fold_rev implies_intr (map cprop_of newgoals @ steps)
-                 |> Drule.generalize ([], [Rn])
+      |> fold_rev implies_intr (map cprop_of newgoals @ steps)
+      |> Drule.generalize ([], [Rn])
 
     val nbranches = length branches
     val npres = length pres
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -21,26 +21,27 @@
 (** General stuff **)
 
 fun mk_measures domT mfuns =
-    let 
-        val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))
-        val mlexT = (domT --> HOLogic.natT) --> relT --> relT
-        fun mk_ms [] = Const (@{const_name Set.empty}, relT)
-          | mk_ms (f::fs) = 
-            Const (@{const_name mlex_prod}, mlexT) $ f $ mk_ms fs
-    in
-        mk_ms mfuns
-    end
+  let
+    val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))
+    val mlexT = (domT --> HOLogic.natT) --> relT --> relT
+    fun mk_ms [] = Const (@{const_name Set.empty}, relT)
+      | mk_ms (f::fs) =
+        Const (@{const_name mlex_prod}, mlexT) $ f $ mk_ms fs
+  in
+    mk_ms mfuns
+  end
 
 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)
 
 (** Matrix cell datatype **)
 
-datatype cell = Less of thm| LessEq of (thm * thm) | None of (thm * thm) | False of thm;
+datatype cell =
+  Less of thm| LessEq of (thm * thm) | None of (thm * thm) | False of thm;
 
 fun is_Less (Less _) = true
   | is_Less _ = false
@@ -57,39 +58,39 @@
 (** Proof attempts to build the matrix **)
 
 fun dest_term (t : term) =
-    let
-      val (vars, prop) = Function_Lib.dest_all_all t
-      val (prems, concl) = Logic.strip_horn prop
-      val (lhs, rhs) = concl
-                         |> HOLogic.dest_Trueprop
-                         |> HOLogic.dest_mem |> fst
-                         |> HOLogic.dest_prod
-    in
-      (vars, prems, lhs, rhs)
-    end
+  let
+    val (vars, prop) = Function_Lib.dest_all_all t
+    val (prems, concl) = Logic.strip_horn prop
+    val (lhs, rhs) = concl
+      |> HOLogic.dest_Trueprop
+      |> HOLogic.dest_mem |> fst
+      |> HOLogic.dest_prod
+  in
+    (vars, prems, lhs, rhs)
+  end
 
 fun mk_goal (vars, prems, lhs, rhs) rel =
-    let
-      val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
-    in
-      fold_rev Logic.all vars (Logic.list_implies (prems, concl))
-    end
+  let
+    val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
+  in
+    fold_rev Logic.all vars (Logic.list_implies (prems, concl))
+  end
 
 fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun =
-    let
-      val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
-    in
-      case try_proof (goals @{const_name HOL.less}) solve_tac of
-        Solved thm => Less thm
-      | Stuck thm => 
-        (case try_proof (goals @{const_name HOL.less_eq}) solve_tac of
-           Solved thm2 => LessEq (thm2, thm)
-         | Stuck thm2 => 
-           if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2
-           else None (thm2, thm)
-         | _ => raise Match) (* FIXME *)
-      | _ => raise Match
-    end
+  let
+    val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
+  in
+    case try_proof (goals @{const_name HOL.less}) solve_tac of
+      Solved thm => Less thm
+    | Stuck thm =>
+      (case try_proof (goals @{const_name HOL.less_eq}) solve_tac of
+         Solved thm2 => LessEq (thm2, thm)
+       | Stuck thm2 =>
+         if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2
+         else None (thm2, thm)
+       | _ => raise Match) (* FIXME *)
+    | _ => raise Match
+  end
 
 
 (** Search algorithms **)
@@ -102,21 +103,21 @@
 
 (* simple depth-first search algorithm for the table *)
 fun search_table table =
-    case table of
-      [] => SOME []
-    | _ =>
-      let
-        val col = find_index (check_col) (transpose table)
-      in case col of
-           ~1 => NONE
-         | _ =>
-           let
-             val order_opt = (table, col) |-> transform_table |> search_table
-           in case order_opt of
-                NONE => NONE
-              | SOME order =>SOME (col :: transform_order col order)
-           end
-      end
+  case table of
+    [] => SOME []
+  | _ =>
+    let
+      val col = find_index (check_col) (transpose table)
+    in case col of
+         ~1 => NONE
+       | _ =>
+         let
+           val order_opt = (table, col) |-> transform_table |> search_table
+         in case order_opt of
+              NONE => NONE
+            | SOME order =>SOME (col :: transform_order col order)
+         end
+    end
 
 (** Proof Reconstruction **)
 
@@ -134,9 +135,9 @@
 (** Error reporting **)
 
 fun pr_goals ctxt st =
-    Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
-     |> Pretty.chunks
-     |> Pretty.string_of
+  Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
+  |> Pretty.chunks
+  |> Pretty.string_of
 
 fun row_index i = chr (i + 97)
 fun col_index j = string_of_int (j + 1)
@@ -151,65 +152,67 @@
       "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
 
 fun pr_unprovable_subgoals ctxt table =
-    table
-     |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs)
-     |> flat
-     |> map (pr_unprovable_cell ctxt)
+  table
+  |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs)
+  |> flat
+  |> map (pr_unprovable_cell ctxt)
 
 fun no_order_msg ctxt table tl measure_funs =
-    let
-      val prterm = Syntax.string_of_term ctxt
-      fun pr_fun t i = string_of_int i ^ ") " ^ prterm t
+  let
+    val prterm = Syntax.string_of_term ctxt
+    fun pr_fun t i = string_of_int i ^ ") " ^ prterm t
 
-      fun pr_goal t i =
-          let
-            val (_, _, lhs, rhs) = dest_term t
-          in (* also show prems? *)
-               i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs
-          end
+    fun pr_goal t i =
+      let
+        val (_, _, lhs, rhs) = dest_term t
+      in (* also show prems? *)
+           i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs
+      end
 
-      val gc = map (fn i => chr (i + 96)) (1 upto length table)
-      val mc = 1 upto length measure_funs
-      val tstr = "Result matrix:" ::  ("   " ^ implode (map (enclose " " " " o string_of_int) mc))
-                 :: map2 (fn r => fn i => i ^ ": " ^ implode (map pr_cell r)) table gc
-      val gstr = "Calls:" :: map2 (prefix "  " oo pr_goal) tl gc
-      val mstr = "Measures:" :: map2 (prefix "  " oo pr_fun) measure_funs mc
-      val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table
-    in
-      cat_lines (ustr @ gstr @ mstr @ tstr @ ["", "Could not find lexicographic termination order."])
-    end
+    val gc = map (fn i => chr (i + 96)) (1 upto length table)
+    val mc = 1 upto length measure_funs
+    val tstr = "Result matrix:" ::  ("   " ^ implode (map (enclose " " " " o string_of_int) mc))
+      :: map2 (fn r => fn i => i ^ ": " ^ implode (map pr_cell r)) table gc
+    val gstr = "Calls:" :: map2 (prefix "  " oo pr_goal) tl gc
+    val mstr = "Measures:" :: map2 (prefix "  " oo pr_fun) measure_funs mc
+    val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table
+  in
+    cat_lines (ustr @ gstr @ mstr @ tstr @
+    ["", "Could not find lexicographic termination order."])
+  end
 
 (** The Main Function **)
 
 fun lex_order_tac quiet ctxt solve_tac (st: thm) =
-    let
-      val thy = ProofContext.theory_of ctxt
-      val ((_ $ (_ $ rel)) :: tl) = prems_of st
+  let
+    val thy = ProofContext.theory_of ctxt
+    val ((_ $ (_ $ rel)) :: tl) = prems_of st
 
-      val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
+    val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
 
-      val measure_funs = MeasureFunctions.get_measure_functions ctxt domT (* 1: generate measures *)
+    val measure_funs = (* 1: generate measures *)
+      MeasureFunctions.get_measure_functions ctxt domT
 
-      (* 2: create table *)
-      val table = Par_List.map (fn t => Par_List.map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
-    in
-      case search_table table of
-        NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
-      | SOME order =>
-          let 
-            val clean_table = map (fn x => map (nth x) order) table
-            val relation = mk_measures domT (map (nth measure_funs) order)
-            val _ = if not quiet
-              then writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation))
-              else ()
+    val table = (* 2: create table *)
+      Par_List.map (fn t => Par_List.map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
+  in
+    case search_table table of
+      NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
+    | SOME order =>
+      let
+        val clean_table = map (fn x => map (nth x) order) table
+        val relation = mk_measures domT (map (nth measure_funs) order)
+        val _ = if not quiet
+          then writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation))
+          else ()
 
-          in (* 4: proof reconstruction *)
-            st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
-            THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
-            THEN (rtac @{thm "wf_empty"} 1)
-            THEN EVERY (map prove_row clean_table))
-          end
-    end
+      in (* 4: proof reconstruction *)
+        st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
+        THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
+        THEN (rtac @{thm "wf_empty"} 1)
+        THEN EVERY (map prove_row clean_table))
+      end
+  end
 
 fun lexicographic_order_tac quiet ctxt =
   TRY (Function_Common.apply_termination_rule ctxt 1)
@@ -225,4 +228,3 @@
   #> Context.theory_map (Function_Common.set_termination_prover lexicographic_order)
 
 end;
-
--- a/src/HOL/Tools/Function/measure_functions.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/measure_functions.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -8,26 +8,28 @@
 sig
 
   val get_measure_functions : Proof.context -> typ -> term list
-  val setup : theory -> theory                                                      
+  val setup : theory -> theory
 
 end
 
-structure MeasureFunctions : MEASURE_FUNCTIONS = 
-struct 
+structure MeasureFunctions : MEASURE_FUNCTIONS =
+struct
 
 (** User-declared size functions **)
 structure Measure_Heuristic_Rules = Named_Thms
 (
-  val name = "measure_function" 
-  val description = "Rules that guide the heuristic generation of measure functions"
+  val name = "measure_function"
+  val description =
+    "Rules that guide the heuristic generation of measure functions"
 );
 
-fun mk_is_measures t = Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
+fun mk_is_measure t =
+  Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
 
 fun find_measures ctxt T =
-  DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) 
-    (HOLogic.mk_Trueprop (mk_is_measures (Var (("f",0), T --> HOLogic.natT)))
-      |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init)
+  DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1)
+    (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT)))
+     |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init)
   |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
   |> Seq.list_of
 
@@ -38,13 +40,13 @@
 fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
 
 fun mk_funorder_funs (Type ("+", [fT, sT])) =
-      map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
-    @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
+  map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
+  @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
   | mk_funorder_funs T = [ constant_1 T ]
 
 fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) =
-      map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
-                  (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
+    map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
+      (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
   | mk_ext_base_funs ctxt T = find_measures ctxt T
 
 fun mk_all_measure_funs ctxt (T as Type ("+", _)) =
@@ -56,4 +58,3 @@
 val setup = Measure_Heuristic_Rules.setup
 
 end
-
--- a/src/HOL/Tools/Function/mutual.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -9,13 +9,13 @@
 sig
 
   val prepare_function_mutual : Function_Common.function_config
-                              -> string (* defname *)
-                              -> ((string * typ) * mixfix) list
-                              -> term list
-                              -> local_theory
-                              -> ((thm (* goalstate *)
-                                   * (thm -> Function_Common.function_result) (* proof continuation *)
-                                  ) * local_theory)
+    -> string (* defname *)
+    -> ((string * typ) * mixfix) list
+    -> term list
+    -> local_theory
+    -> ((thm (* goalstate *)
+        * (thm -> Function_Common.function_result) (* proof continuation *)
+       ) * local_theory)
 
 end
 
@@ -28,282 +28,269 @@
 
 type qgar = string * (string * typ) list * term list * term list * term
 
-datatype mutual_part =
-  MutualPart of 
-   {
-    i : int,
-    i' : int,
-    fvar : string * typ,
-    cargTs: typ list,
-    f_def: term,
+datatype mutual_part = MutualPart of
+ {i : int,
+  i' : int,
+  fvar : string * typ,
+  cargTs: typ list,
+  f_def: term,
 
-    f: term option,
-    f_defthm : thm option
-   }
-   
+  f: term option,
+  f_defthm : thm option}
 
-datatype mutual_info =
-  Mutual of 
-   { 
-    n : int,
-    n' : int,
-    fsum_var : string * typ,
+datatype mutual_info = Mutual of
+ {n : int,
+  n' : int,
+  fsum_var : string * typ,
 
-    ST: typ,
-    RST: typ,
+  ST: typ,
+  RST: typ,
 
-    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}
 
 fun mutual_induct_Pnames n =
-    if n < 5 then fst (chop n ["P","Q","R","S"])
-    else map (fn i => "P" ^ string_of_int i) (1 upto n)
+  if n < 5 then fst (chop n ["P","Q","R","S"])
+  else map (fn i => "P" ^ string_of_int i) (1 upto n)
 
 fun get_part fname =
-    the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname)
-                     
+  the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname)
+
 (* FIXME *)
 fun mk_prod_abs e (t1, t2) =
-    let
-      val bTs = rev (map snd e)
-      val T1 = fastype_of1 (bTs, t1)
-      val T2 = fastype_of1 (bTs, t2)
-    in
-      HOLogic.pair_const T1 T2 $ t1 $ t2
-    end;
-
+  let
+    val bTs = rev (map snd e)
+    val T1 = fastype_of1 (bTs, t1)
+    val T2 = fastype_of1 (bTs, t2)
+  in
+    HOLogic.pair_const T1 T2 $ t1 $ t2
+  end
 
 fun analyze_eqs ctxt defname fs eqs =
-    let
-      val num = length fs
-        val fqgars = map (split_def ctxt) eqs
-        val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
-                       |> AList.lookup (op =) #> the
+  let
+    val num = length fs
+    val fqgars = map (split_def ctxt) eqs
+    val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
+      |> AList.lookup (op =) #> the
 
-        fun curried_types (fname, fT) =
-            let
-              val (caTs, uaTs) = chop (arity_of fname) (binder_types fT)
-            in
-                (caTs, uaTs ---> body_type fT)
-            end
+    fun curried_types (fname, fT) =
+      let
+        val (caTs, uaTs) = chop (arity_of fname) (binder_types fT)
+      in
+        (caTs, uaTs ---> body_type fT)
+      end
 
-        val (caTss, resultTs) = split_list (map curried_types fs)
-        val argTs = map (foldr1 HOLogic.mk_prodT) caTss
+    val (caTss, resultTs) = split_list (map curried_types fs)
+    val argTs = map (foldr1 HOLogic.mk_prodT) caTss
 
-        val dresultTs = distinct (op =) resultTs
-        val n' = length dresultTs
+    val dresultTs = distinct (op =) resultTs
+    val n' = length dresultTs
 
-        val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs
-        val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs
+    val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs
+    val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs
 
-        val fsum_type = ST --> RST
+    val fsum_type = ST --> RST
 
-        val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
-        val fsum_var = (fsum_var_name, fsum_type)
+    val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
+    val fsum_var = (fsum_var_name, fsum_type)
 
-        fun define (fvar as (n, _)) caTs resultT i =
-            let
-                val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
-                val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 
+    fun define (fvar as (n, _)) caTs resultT i =
+      let
+        val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
+        val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1
 
-                val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
-                val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)
+        val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
+        val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)
 
-                val rew = (n, fold_rev lambda vars f_exp)
-            in
-                (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew)
-            end
-            
-        val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num))
+        val rew = (n, fold_rev lambda vars f_exp)
+      in
+        (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew)
+      end
+
+    val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num))
 
-        fun convert_eqs (f, qs, gs, args, rhs) =
-            let
-              val MutualPart {i, i', ...} = get_part f parts
-            in
-              (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
-               SumTree.mk_inj RST n' i' (replace_frees rews rhs)
-                               |> Envir.beta_norm)
-            end
+    fun convert_eqs (f, qs, gs, args, rhs) =
+      let
+        val MutualPart {i, i', ...} = get_part f parts
+      in
+        (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
+         SumTree.mk_inj RST n' i' (replace_frees rews rhs)
+         |> Envir.beta_norm)
+      end
 
-        val qglrs = map convert_eqs fqgars
-    in
-        Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, 
-                parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE}
-    end
-
-
-
+    val qglrs = map convert_eqs fqgars
+  in
+    Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST,
+      parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE}
+  end
 
 fun define_projections fixes mutual fsum lthy =
-    let
-      fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
-          let
-            val ((f, (_, f_defthm)), lthy') =
-              Local_Theory.define
-                ((Binding.name fname, mixfix),
-                  ((Binding.conceal (Binding.name (fname ^ "_def")), []),
-                  Term.subst_bound (fsum, f_def))) lthy
-          in
-            (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
-                         f=SOME f, f_defthm=SOME f_defthm },
-             lthy')
-          end
-          
-      val Mutual { n, n', fsum_var, ST, RST, parts, fqgars, qglrs, ... } = mutual
-      val (parts', lthy') = fold_map def (parts ~~ fixes) lthy
-    in
-      (Mutual { n=n, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts',
-                fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum },
-       lthy')
-    end
+  let
+    fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
+      let
+        val ((f, (_, f_defthm)), lthy') =
+          Local_Theory.define
+            ((Binding.name fname, mixfix),
+              ((Binding.conceal (Binding.name (fname ^ "_def")), []),
+              Term.subst_bound (fsum, f_def))) lthy
+      in
+        (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
+           f=SOME f, f_defthm=SOME f_defthm },
+         lthy')
+      end
 
+    val Mutual { n, n', fsum_var, ST, RST, parts, fqgars, qglrs, ... } = mutual
+    val (parts', lthy') = fold_map def (parts ~~ fixes) lthy
+  in
+    (Mutual { n=n, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts',
+       fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum },
+     lthy')
+  end
 
 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, _) = Variable.variant_fixes oqnames ctxt
-        |>> 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
-      val rhs = inst pre_rhs
+  let
+    val thy = ProofContext.theory_of ctxt
+
+    val oqnames = map fst pre_qs
+    val (qs, _) = Variable.variant_fixes oqnames ctxt
+      |>> 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
+    val rhs = inst pre_rhs
 
-      val cqs = map (cterm_of thy) qs
-      val ags = map (assume o cterm_of thy) gs
+    val cqs = map (cterm_of thy) qs
+    val ags = map (assume o cterm_of thy) gs
 
-      val import = fold forall_elim cqs
-                   #> fold Thm.elim_implies ags
+    val import = fold forall_elim cqs
+      #> fold Thm.elim_implies ags
 
-      val export = fold_rev (implies_intr o cprop_of) ags
-                   #> fold_rev forall_intr_rename (oqnames ~~ cqs)
-    in
-      F ctxt (f, qs, gs, args, rhs) import export
-    end
-
-fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) import (export : thm -> thm) sum_psimp_eq =
-    let
-      val (MutualPart {f=SOME f, ...}) = get_part fname parts
+    val export = fold_rev (implies_intr o cprop_of) ags
+      #> fold_rev forall_intr_rename (oqnames ~~ cqs)
+  in
+    F ctxt (f, qs, gs, args, rhs) import export
+  end
 
-      val psimp = import sum_psimp_eq
-      val (simp, restore_cond) = case cprems_of psimp of
-                                   [] => (psimp, I)
-                                 | [cond] => (implies_elim psimp (assume cond), implies_intr cond)
-                                 | _ => sys_error "Too many conditions"
-    in
-      Goal.prove ctxt [] [] 
-                 (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
-                 (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs)
-                          THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
-                          THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
-        |> restore_cond 
-        |> export
-    end
+fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs)
+  import (export : thm -> thm) sum_psimp_eq =
+  let
+    val (MutualPart {f=SOME f, ...}) = get_part fname parts
+
+    val psimp = import sum_psimp_eq
+    val (simp, restore_cond) =
+      case cprems_of psimp of
+        [] => (psimp, I)
+      | [cond] => (implies_elim psimp (assume cond), implies_intr cond)
+      | _ => sys_error "Too many conditions"
 
+  in
+    Goal.prove ctxt [] []
+      (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
+      (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs)
+         THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
+         THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
+    |> restore_cond
+    |> export
+  end
 
-(* FIXME HACK *)
 fun mk_applied_form ctxt caTs thm =
-    let
-      val thy = ProofContext.theory_of ctxt
-      val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
-    in
-      fold (fn x => fn thm => combination thm (reflexive x)) xs thm
-           |> Conv.fconv_rule (Thm.beta_conversion true)
-           |> fold_rev forall_intr xs
-           |> Thm.forall_elim_vars 0
-    end
-
+  let
+    val thy = ProofContext.theory_of ctxt
+    val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
+  in
+    fold (fn x => fn thm => combination thm (reflexive x)) xs thm
+    |> Conv.fconv_rule (Thm.beta_conversion true)
+    |> fold_rev forall_intr xs
+    |> Thm.forall_elim_vars 0
+  end
 
 fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, parts, ...}) =
-    let
-      val cert = cterm_of (ProofContext.theory_of lthy)
-      val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => 
-                                       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 = SumTree.mk_sumcases HOLogic.boolT Ps
-                     
-      val induct_inst =
-          forall_elim (cert case_exp) induct
-                      |> full_simplify SumTree.sumcase_split_ss
-                      |> full_simplify (HOL_basic_ss addsimps all_f_defs)
-          
-      fun project rule (MutualPart {cargTs, i, ...}) k =
-          let
-            val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *)
-            val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
-          in
-            (rule
-              |> forall_elim (cert inj)
-              |> full_simplify SumTree.sumcase_split_ss
-              |> fold_rev (forall_intr o cert) (afs @ newPs),
-             k + length cargTs)
-          end
-    in
-      fst (fold_map (project induct_inst) parts 0)
-    end
-    
+  let
+    val cert = cterm_of (ProofContext.theory_of lthy)
+    val newPs =
+      map2 (fn Pname => fn MutualPart {cargTs, ...} =>
+          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 = SumTree.mk_sumcases HOLogic.boolT Ps
+
+    val induct_inst =
+      forall_elim (cert case_exp) induct
+      |> full_simplify SumTree.sumcase_split_ss
+      |> full_simplify (HOL_basic_ss addsimps all_f_defs)
+
+    fun project rule (MutualPart {cargTs, i, ...}) k =
+      let
+        val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *)
+        val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
+      in
+        (rule
+         |> forall_elim (cert inj)
+         |> full_simplify SumTree.sumcase_split_ss
+         |> fold_rev (forall_intr o cert) (afs @ newPs),
+         k + length cargTs)
+      end
+  in
+    fst (fold_map (project induct_inst) parts 0)
+  end
 
 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
-    let
-      val result = inner_cont proof
-      val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
-        termination, domintros, ...} = result
-                                                                                                               
-      val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
-                                     (mk_applied_form lthy cargTs (symmetric f_def), f))
-                                 parts
-                             |> split_list
+  let
+    val result = inner_cont proof
+    val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
+      termination, domintros, ...} = result
+
+    val (all_f_defs, fs) =
+      map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
+        (mk_applied_form lthy cargTs (symmetric f_def), f))
+      parts
+      |> split_list
+
+    val all_orig_fdefs =
+      map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts
+
+    fun mk_mpsimp fqgar sum_psimp =
+      in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp
 
-      val all_orig_fdefs = map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts
-                           
-      fun mk_mpsimp fqgar sum_psimp =
-          in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp
-          
-      val rew_ss = HOL_basic_ss addsimps all_f_defs
-      val mpsimps = map2 mk_mpsimp fqgars psimps
-      val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps
-      val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
-      val mtermination = full_simplify rew_ss termination
-      val mdomintros = map_option (map (full_simplify rew_ss)) domintros
-    in
-      FunctionResult { fs=fs, G=G, R=R,
-                     psimps=mpsimps, simple_pinducts=minducts,
-                     cases=cases, termination=mtermination,
-                     domintros=mdomintros,
-                     trsimps=mtrsimps}
-    end
-      
+    val rew_ss = HOL_basic_ss addsimps all_f_defs
+    val mpsimps = map2 mk_mpsimp fqgars psimps
+    val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps
+    val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
+    val mtermination = full_simplify rew_ss termination
+    val mdomintros = map_option (map (full_simplify rew_ss)) domintros
+  in
+    FunctionResult { fs=fs, G=G, R=R,
+      psimps=mpsimps, simple_pinducts=minducts,
+      cases=cases, termination=mtermination,
+      domintros=mdomintros, trsimps=mtrsimps}
+  end
+
 fun prepare_function_mutual config defname fixes eqss lthy =
-    let
-      val mutual = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
-      val Mutual {fsum_var=(n, T), qglrs, ...} = mutual
-          
-      val ((fsum, goalstate, cont), lthy') =
-          Function_Core.prepare_function config defname [((n, T), NoSyn)] qglrs lthy
-          
-      val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
+  let
+    val mutual as Mutual {fsum_var=(n, T), qglrs, ...} =
+      analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
+
+    val ((fsum, goalstate, cont), lthy') =
+      Function_Core.prepare_function config defname [((n, T), NoSyn)] qglrs lthy
 
-      val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual'
-    in
-      ((goalstate, mutual_cont), lthy'')
-    end
+    val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
 
-    
+    val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual'
+  in
+    ((goalstate, mutual_cont), lthy'')
+  end
+
 end
--- a/src/HOL/Tools/Function/pattern_split.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/pattern_split.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -1,10 +1,7 @@
 (*  Title:      HOL/Tools/Function/pattern_split.ML
     Author:     Alexander Krauss, TU Muenchen
 
-A package for general recursive function definitions.
-
-Automatic splitting of overlapping constructor patterns. This is a preprocessing step which
-turns a specification with overlaps into an overlap-free specification.
+Fairly ad-hoc pattern splitting.
 
 *)
 
@@ -22,114 +19,102 @@
 
 open Function_Lib
 
-(* We use proof context for the variable management *)
-(* FIXME: no __ *)
-
 fun new_var ctx vs T =
-    let
-      val [v] = Variable.variant_frees ctx vs [("v", T)]
-    in
-      (Free v :: vs, Free v)
-    end
+  let
+    val [v] = Variable.variant_frees ctx vs [("v", T)]
+  in
+    (Free v :: vs, Free v)
+  end
 
 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" *)
+  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 "pat_completeness.ML" *)
 fun inst_constrs_of thy (T as Type (name, _)) =
-    map (fn (Cn,CT) =>
-          Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
-        (the (Datatype.get_constrs thy name))
+  map (fn (Cn,CT) =>
+    Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+    (the (Datatype.get_constrs thy name))
   | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
-                            
-                            
-                            
+
 
 fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
 fun join_product (xs, ys) = map_product (curry join) xs ys
 
-
 exception DISJ
 
 fun pattern_subtract_subst ctx vs t t' =
-    let
-      exception DISJ
-      fun pattern_subtract_subst_aux vs _ (Free v2) = []
-        | pattern_subtract_subst_aux vs (v as (Free (_, T))) t' =
+  let
+    exception DISJ
+    fun pattern_subtract_subst_aux vs _ (Free v2) = []
+      | pattern_subtract_subst_aux vs (v as (Free (_, T))) t' =
+      let
+        fun foo constr =
           let
-            fun foo constr =
-                let
-                  val (vs', t) = saturate ctx vs constr
-                  val substs = pattern_subtract_subst ctx vs' t t'
-                in
-                  map (fn (vs, subst) => (vs, (v,t)::subst)) substs
-                end
+            val (vs', t) = saturate ctx vs constr
+            val substs = pattern_subtract_subst ctx vs' t t'
           in
-            maps foo (inst_constrs_of (ProofContext.theory_of ctx) T)
+            map (fn (vs, subst) => (vs, (v,t)::subst)) substs
           end
-        | pattern_subtract_subst_aux vs t t' =
-          let
-            val (C, ps) = strip_comb t
-            val (C', qs) = strip_comb t'
-          in
-            if C = C'
-            then flat (map2 (pattern_subtract_subst_aux vs) ps qs)
-            else raise DISJ
-          end
-    in
-      pattern_subtract_subst_aux vs t t'
-      handle DISJ => [(vs, [])]
-    end
-
+      in
+        maps foo (inst_constrs_of (ProofContext.theory_of ctx) T)
+      end
+     | pattern_subtract_subst_aux vs t t' =
+     let
+       val (C, ps) = strip_comb t
+       val (C', qs) = strip_comb t'
+     in
+       if C = C'
+       then flat (map2 (pattern_subtract_subst_aux vs) ps qs)
+       else raise DISJ
+     end
+  in
+    pattern_subtract_subst_aux vs t t'
+    handle DISJ => [(vs, [])]
+  end
 
 (* p - q *)
 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
-          in
-            fold_rev Logic.all (inter (op =) vs' (map Free (frees_in_term ctx t))) t
-          end
-    in
-      map instantiate substs
-    end
-      
+  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
+      in
+        fold_rev Logic.all (inter (op =) vs' (map Free (frees_in_term ctx t))) t
+      end
+  in
+    map instantiate substs
+  end
 
 (* ps - p' *)
 fun pattern_subtract_from_many ctx p'=
-    maps (pattern_subtract ctx p')
+  maps (pattern_subtract ctx p')
 
 (* in reverse order *)
 fun pattern_subtract_many ctx ps' =
-    fold_rev (pattern_subtract_from_many ctx) ps'
-
-
+  fold_rev (pattern_subtract_from_many ctx) ps'
 
 fun split_some_equations ctx eqns =
-    let
-      fun split_aux prev [] = []
-        | split_aux prev ((true, eq) :: es) = pattern_subtract_many ctx prev [eq]
-                                              :: split_aux (eq :: prev) es
-        | split_aux prev ((false, eq) :: es) = [eq]
-                                               :: split_aux (eq :: prev) es
-    in
-      split_aux [] eqns
-    end
-    
+  let
+    fun split_aux prev [] = []
+      | split_aux prev ((true, eq) :: es) =
+        pattern_subtract_many ctx prev [eq] :: split_aux (eq :: prev) es
+      | split_aux prev ((false, eq) :: es) =
+        [eq] :: split_aux (eq :: prev) es
+  in
+    split_aux [] eqns
+  end
+
 fun split_all_equations ctx =
-    split_some_equations ctx o map (pair true)
-
-
+  split_some_equations ctx o map (pair true)
 
 
 end
--- a/src/HOL/Tools/Function/relation.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/relation.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -15,18 +15,18 @@
 struct
 
 fun inst_thm ctxt rel st =
-    let
-      val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
-      val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
-      val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
-      val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') [])))
-    in 
-      Drule.cterm_instantiate [(Rvar, rel')] st' 
-    end
+  let
+    val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
+    val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
+    val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
+    val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') [])))
+  in
+    Drule.cterm_instantiate [(Rvar, rel')] st'
+  end
 
-fun relation_tac ctxt rel i = 
-    TRY (Function_Common.apply_termination_rule ctxt i)
-    THEN PRIMITIVE (inst_thm ctxt rel)
+fun relation_tac ctxt rel i =
+  TRY (Function_Common.apply_termination_rule ctxt i)
+  THEN PRIMITIVE (inst_thm ctxt rel)
 
 val setup =
   Method.setup @{binding relation}
--- a/src/HOL/Tools/Function/sum_tree.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/sum_tree.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -9,35 +9,43 @@
 
 (* Theory dependencies *)
 val proj_in_rules = [@{thm Projl_Inl}, @{thm Projr_Inr}]
-val sumcase_split_ss = HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases})
+val sumcase_split_ss =
+  HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases})
 
 (* top-down access in balanced tree *)
 fun access_top_down {left, right, init} len i =
-    Balanced_Tree.access {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
+  Balanced_Tree.access
+    {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
 
 (* Sum types *)
 fun mk_sumT LT RT = Type ("+", [LT, RT])
-fun mk_sumcase TL TR T l r = Const (@{const_name sum.sum_case}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
+fun mk_sumcase TL TR T l r =
+  Const (@{const_name sum.sum_case},
+    (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
 
 val App = curry op $
 
-fun mk_inj ST n i = 
-    access_top_down 
-    { init = (ST, I : term -> term),
-      left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, inj o App (Const (@{const_name Inl}, LT --> T)))),
-      right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i 
-    |> snd
+fun mk_inj ST n i =
+  access_top_down
+  { init = (ST, I : term -> term),
+    left = (fn (T as Type ("+", [LT, RT]), inj) =>
+      (LT, inj o App (Const (@{const_name Inl}, LT --> T)))),
+    right =(fn (T as Type ("+", [LT, RT]), inj) =>
+      (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i
+  |> snd
 
-fun mk_proj ST n i = 
-    access_top_down 
-    { init = (ST, I : term -> term),
-      left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)),
-      right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i
-    |> snd
+fun mk_proj ST n i =
+  access_top_down
+  { init = (ST, I : term -> term),
+    left = (fn (T as Type ("+", [LT, RT]), proj) =>
+      (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)),
+    right =(fn (T as Type ("+", [LT, RT]), proj) =>
+      (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i
+  |> snd
 
 fun mk_sumcases T fs =
-      Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) 
-                        (map (fn f => (f, domain_type (fastype_of f))) fs)
-      |> fst
+  Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) 
+    (map (fn f => (f, domain_type (fastype_of f))) fs)
+  |> fst
 
 end
--- a/src/HOL/Tools/Function/termination.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/termination.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -245,66 +245,65 @@
 (* A tactic to convert open to closed termination goals *)
 local
 fun dest_term (t : term) = (* FIXME, cf. Lexicographic order *)
-    let
-      val (vars, prop) = Function_Lib.dest_all_all t
-      val (prems, concl) = Logic.strip_horn prop
-      val (lhs, rhs) = concl
-                         |> HOLogic.dest_Trueprop
-                         |> HOLogic.dest_mem |> fst
-                         |> HOLogic.dest_prod
-    in
-      (vars, prems, lhs, rhs)
-    end
+  let
+    val (vars, prop) = Function_Lib.dest_all_all t
+    val (prems, concl) = Logic.strip_horn prop
+    val (lhs, rhs) = concl
+      |> HOLogic.dest_Trueprop
+      |> HOLogic.dest_mem |> fst
+      |> HOLogic.dest_prod
+  in
+    (vars, prems, lhs, rhs)
+  end
 
 fun mk_pair_compr (T, qs, l, r, conds) =
-    let
-      val pT = HOLogic.mk_prodT (T, T)
-      val n = length qs
-      val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r)
-      val conds' = if null conds then [HOLogic.true_const] else conds
-    in
-      HOLogic.Collect_const pT $
-      Abs ("uu_", pT,
-           (foldr1 HOLogic.mk_conj (peq :: conds')
-            |> fold_rev (fn v => fn t => HOLogic.exists_const (fastype_of v) $ lambda v t) qs))
-    end
+  let
+    val pT = HOLogic.mk_prodT (T, T)
+    val n = length qs
+    val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r)
+    val conds' = if null conds then [HOLogic.true_const] else conds
+  in
+    HOLogic.Collect_const pT $
+    Abs ("uu_", pT,
+      (foldr1 HOLogic.mk_conj (peq :: conds')
+      |> fold_rev (fn v => fn t => HOLogic.exists_const (fastype_of v) $ lambda v t) qs))
+  end
 
 in
 
 fun wf_union_tac ctxt st =
-    let
-      val thy = ProofContext.theory_of ctxt
-      val cert = cterm_of (theory_of_thm st)
-      val ((_ $ (_ $ rel)) :: ineqs) = prems_of st
+  let
+    val thy = ProofContext.theory_of ctxt
+    val cert = cterm_of (theory_of_thm st)
+    val ((_ $ (_ $ rel)) :: ineqs) = prems_of st
 
-      fun mk_compr ineq =
-          let
-            val (vars, prems, lhs, rhs) = dest_term ineq
-          in
-            mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (ObjectLogic.atomize_term thy) prems)
-          end
+    fun mk_compr ineq =
+      let
+        val (vars, prems, lhs, rhs) = dest_term ineq
+      in
+        mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (ObjectLogic.atomize_term thy) prems)
+      end
 
-      val relation =
-          if null ineqs then
-              Const (@{const_name Set.empty}, fastype_of rel)
-          else
-              foldr1 (HOLogic.mk_binop @{const_name Lattices.sup}) (map mk_compr ineqs)
+    val relation =
+      if null ineqs
+      then Const (@{const_name Set.empty}, fastype_of rel)
+      else map mk_compr ineqs
+        |> foldr1 (HOLogic.mk_binop @{const_name Lattices.sup})
 
-      fun solve_membership_tac i =
-          (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
-          THEN' (fn j => TRY (rtac @{thm UnI1} j))
-          THEN' (rtac @{thm CollectI})                    (* unfold comprehension *)
-          THEN' (fn i => REPEAT (rtac @{thm exI} i))      (* Turn existentials into schematic Vars *)
-          THEN' ((rtac @{thm refl})                       (* unification instantiates all Vars *)
-                 ORELSE' ((rtac @{thm conjI})
-                          THEN' (rtac @{thm refl})
-                          THEN' (blast_tac (claset_of ctxt))))  (* Solve rest of context... not very elegant *)
-          ) i
-    in
-      ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
-      THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i))) st
-    end
-
+    fun solve_membership_tac i =
+      (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
+      THEN' (fn j => TRY (rtac @{thm UnI1} j))
+      THEN' (rtac @{thm CollectI})                    (* unfold comprehension *)
+      THEN' (fn i => REPEAT (rtac @{thm exI} i))      (* Turn existentials into schematic Vars *)
+      THEN' ((rtac @{thm refl})                       (* unification instantiates all Vars *)
+        ORELSE' ((rtac @{thm conjI})
+          THEN' (rtac @{thm refl})
+          THEN' (blast_tac (claset_of ctxt))))  (* Solve rest of context... not very elegant *)
+      ) i
+  in
+    ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
+     THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i))) st
+  end
 
 end
 
@@ -332,67 +331,65 @@
 
 fun derive_chains ctxt chain_tac cont D = CALLS (fn (cs, i) =>
   let
-      val thy = ProofContext.theory_of ctxt
+    val thy = ProofContext.theory_of ctxt
 
-      fun derive_chain c1 c2 D =
-        if is_some (get_chain D c1 c2) then D else
-        note_chain c1 c2 (prove_chain thy chain_tac c1 c2) D
+    fun derive_chain c1 c2 D =
+      if is_some (get_chain D c1 c2) then D else
+      note_chain c1 c2 (prove_chain thy chain_tac c1 c2) D
   in
     cont (fold_product derive_chain cs cs D) i
   end)
 
 
 fun mk_dgraph D cs =
-    TermGraph.empty
-    |> fold (fn c => TermGraph.new_node (c,())) cs
-    |> fold_product (fn c1 => fn c2 =>
-         if is_none (get_chain D c1 c2 |> the_default NONE)
-         then TermGraph.add_edge (c1, c2) else I)
-       cs cs
-
+  TermGraph.empty
+  |> fold (fn c => TermGraph.new_node (c,())) cs
+  |> fold_product (fn c1 => fn c2 =>
+     if is_none (get_chain D c1 c2 |> the_default NONE)
+     then TermGraph.add_edge (c1, c2) else I)
+     cs cs
 
 fun ucomp_empty_tac T =
-    REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR}
-                    ORELSE' rtac @{thm union_comp_emptyL}
-                    ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i))
+  REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR}
+    ORELSE' rtac @{thm union_comp_emptyL}
+    ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i))
 
 fun regroup_calls_tac cs = CALLS (fn (cs', i) =>
-   let
-     val is = map (fn c => find_index (curry op aconv c) cs') cs
-   in
-     CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv is))) i
-   end)
+ let
+   val is = map (fn c => find_index (curry op aconv c) cs') cs
+ in
+   CONVERSION (Conv.arg_conv (Conv.arg_conv
+     (Function_Lib.regroup_union_conv is))) i
+ end)
 
 
-fun solve_trivial_tac D = CALLS
-(fn ([c], i) =>
-    (case get_chain D c c of
-       SOME (SOME thm) => rtac @{thm wf_no_loop} i
-                          THEN rtac thm i
-     | _ => no_tac)
+fun solve_trivial_tac D = CALLS (fn ([c], i) =>
+  (case get_chain D c c of
+     SOME (SOME thm) => rtac @{thm wf_no_loop} i
+                        THEN rtac thm i
+   | _ => no_tac)
   | _ => no_tac)
 
 fun decompose_tac' cont err_cont D = CALLS (fn (cs, i) =>
-    let
-      val G = mk_dgraph D cs
-      val sccs = TermGraph.strong_conn G
+  let
+    val G = mk_dgraph D cs
+    val sccs = TermGraph.strong_conn G
 
-      fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i)
-        | split (SCC::rest) i =
-            regroup_calls_tac SCC i
-            THEN rtac @{thm wf_union_compatible} i
-            THEN rtac @{thm less_by_empty} (i + 2)
-            THEN ucomp_empty_tac (the o the oo get_chain D) (i + 2)
-            THEN split rest (i + 1)
-            THEN (solve_trivial_tac D i ORELSE cont D i)
-    in
-      if length sccs > 1 then split sccs i
-      else solve_trivial_tac D i ORELSE err_cont D i
-    end)
+    fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i)
+      | split (SCC::rest) i =
+        regroup_calls_tac SCC i
+        THEN rtac @{thm wf_union_compatible} i
+        THEN rtac @{thm less_by_empty} (i + 2)
+        THEN ucomp_empty_tac (the o the oo get_chain D) (i + 2)
+        THEN split rest (i + 1)
+        THEN (solve_trivial_tac D i ORELSE cont D i)
+  in
+    if length sccs > 1 then split sccs i
+    else solve_trivial_tac D i ORELSE err_cont D i
+  end)
 
 fun decompose_tac ctxt chain_tac cont err_cont =
-    derive_chains ctxt chain_tac
-    (decompose_tac' cont err_cont)
+  derive_chains ctxt chain_tac (decompose_tac' cont err_cont)
 
 
 (*** Local Descent Proofs ***)