--- a/CookBook/Package/simple_inductive_package.ML	Tue Feb 17 13:53:54 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML	Wed Feb 18 17:17:37 2009 +0000
@@ -60,31 +60,31 @@
 (* @chunk induction_rules *)
 fun INDUCTION rules preds' Tss defs lthy1 lthy2 =
 let
-    val (Pnames, lthy3) = Variable.variant_fixes (replicate (length preds') "P") lthy2;
-    val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) (Pnames ~~ Tss);
-    val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps;
-    val rules'' = map (subst_free (preds' ~~ Ps)) rules;
+  val (Pnames, lthy3) = Variable.variant_fixes (replicate (length preds') "P") lthy2;
+  val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) (Pnames ~~ Tss);
+  val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps;
+  val rules'' = map (subst_free (preds' ~~ Ps)) rules;
 
-    fun prove_indrule ((R, P), Ts)  =
-      let
-        val (znames, lthy4) = Variable.variant_fixes (replicate (length Ts) "z") lthy3;
-        val zs = map Free (znames ~~ Ts)
+  fun prove_indrule ((R, P), Ts)  =
+  let
+    val (znames, lthy4) = Variable.variant_fixes (replicate (length Ts) "z") lthy3;
+    val zs = map Free (znames ~~ Ts)
 
-        val prem = HOLogic.mk_Trueprop (list_comb (R, zs))
-        val goal = Logic.list_implies (rules'', HOLogic.mk_Trueprop (list_comb (P, zs)))
-      in
-        Goal.prove lthy4 [] [prem] goal
-          (fn {prems, ...} => EVERY1
-             ([ObjectLogic.full_atomize_tac,
-               cut_facts_tac prems,
-               K (rewrite_goals_tac defs)] @
-              map (fn ct => dtac (inst_spec ct)) cPs @
-              [assume_tac])) |>
-           singleton (ProofContext.export lthy4 lthy1)
-      end;
+    val prem = HOLogic.mk_Trueprop (list_comb (R, zs))
+    val goal = Logic.list_implies (rules'', HOLogic.mk_Trueprop (list_comb (P, zs)))
+  in
+    Goal.prove lthy4 [] [prem] goal
+      (fn {prems, ...} => EVERY1
+         ([ObjectLogic.full_atomize_tac,
+           cut_facts_tac prems,
+           K (rewrite_goals_tac defs)] @
+          map (fn ct => dtac (inst_spec ct)) cPs @
+          [assume_tac])) |>
+       singleton (ProofContext.export lthy4 lthy1)
+  end;
 in
-  map prove_indrule (preds' ~~ Ps ~~ Tss)
-end
+      map prove_indrule (preds' ~~ Ps ~~ Tss)
+  end
 (* @end *)
 
 (* @chunk intro_rules *) 
@@ -123,22 +123,22 @@
 
 (* @chunk add_inductive_i *)
 fun add_inductive_i preds params specs lthy =
-  let
-    val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params;
-    val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.base_name R, T), params')) preds;
-    val Tss = map (binder_types o fastype_of) preds';   
-    val (ass,rules) = split_list specs;    
+let
+  val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params;
+  val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.base_name R, T), params')) preds;
+  val Tss = map (binder_types o fastype_of) preds';   
+  val (ass,rules) = split_list specs;    
 
-    val (defs, lthy1) = definitions params' rules preds preds' Tss lthy
-    val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1;
+  val (defs, lthy1) = definitions params' rules preds preds' Tss lthy
+  val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1;
       
-    val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2
+  val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2
 
-    val intros = INTROS rules preds' defs lthy1 lthy2
+  val intros = INTROS rules preds' defs lthy1 lthy2
 
-    val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds);
-    val case_names = map (Binding.base_name o fst o fst) specs
-  in
+  val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds);
+  val case_names = map (Binding.base_name o fst o fst) specs
+in
     lthy1 
     |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
         ((Binding.qualify mut_name a, atts), [([th], [])])) (specs ~~ intros)) 
@@ -152,7 +152,7 @@
            Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
           (preds ~~ inducts)) #>> maps snd) 
     |> snd
-  end
+end
 (* @end *)
 
 (* @chunk read_specification *)
@@ -184,10 +184,10 @@
    OuterParse.fixes -- 
    OuterParse.for_fixes --
    Scan.optional 
-       (OuterParse.$$$ "where" |--
-          OuterParse.!!! 
-            (OuterParse.enum1 "|" 
-               (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []
+     (OuterParse.$$$ "where" |--
+        OuterParse.!!! 
+          (OuterParse.enum1 "|" 
+             (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []
 (* @end *)
 
 (* @chunk syntax *)