--- a/Nominal-General/nominal_library.ML	Sat Sep 11 05:56:49 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Sun Sep 12 22:46:40 2010 +0800
@@ -100,12 +100,12 @@
 fun sum_case_const ty1 ty2 ty3 = 
   Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)
 fun mk_sum_case trm1 trm2 =
-let
-  val ([ty1], ty3) = strip_type (fastype_of trm1)
-  val ty2 = domain_type (fastype_of trm2)
-in
-  sum_case_const ty1 ty2 ty3 $ trm1 $ trm2
-end 
+  let
+    val ([ty1], ty3) = strip_type (fastype_of trm1)
+    val ty2 = domain_type (fastype_of trm2)
+  in
+    sum_case_const ty1 ty2 ty3 $ trm1 $ trm2
+  end 
 
 
 
@@ -209,19 +209,19 @@
 (* returns the constants of the constructors plus the 
    corresponding type and types of arguments *)
 fun all_dtyp_constrs_types descr sorts = 
-let
-  fun aux ((ty_name, vs), (cname, args)) =
   let
-    val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs
-    val ty = Type (ty_name, vs_tys)
-    val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args
-    val is_rec = map Datatype_Aux.is_rec_type args
+    fun aux ((ty_name, vs), (cname, args)) =
+      let
+        val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs
+        val ty = Type (ty_name, vs_tys)
+        val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args
+        val is_rec = map Datatype_Aux.is_rec_type args
+      in
+        (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec)
+      end
   in
-    (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec)
+    map (map aux) (all_dtyp_constrs_info descr)
   end
-in
-  map (map aux) (all_dtyp_constrs_info descr)
-end
 
 fun nth_dtyp_constrs_types descr sorts n =
   nth (all_dtyp_constrs_types descr sorts) n
@@ -230,45 +230,45 @@
 (* generates for every datatype a name str ^ dt_name 
    plus and index for multiple occurences of a string *)
 fun prefix_dt_names descr sorts str = 
-let
-  fun get_nth_name (i, _) = 
-    Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) 
-in
-  Datatype_Prop.indexify_names 
-    (map (prefix str o get_nth_name) descr)
-end
+  let
+    fun get_nth_name (i, _) = 
+      Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) 
+  in
+    Datatype_Prop.indexify_names 
+      (map (prefix str o get_nth_name) descr)
+  end
 
 
 
 (** function package tactics **)
 
 fun pat_completeness_simp simps lthy =
-let
-  val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps)
-in
-  Pat_Completeness.pat_completeness_tac lthy 1
-    THEN ALLGOALS (asm_full_simp_tac simp_set)
-end
+  let
+    val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps)
+  in
+    Pat_Completeness.pat_completeness_tac lthy 1
+      THEN ALLGOALS (asm_full_simp_tac simp_set)
+  end
 
 fun prove_termination_tac size_simps ctxt i st  =
-let
-  fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
-      SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT)
-    | mk_size_measure T = size_const T
+  let
+    fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
+        SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT)
+      | mk_size_measure T = size_const T
 
-  val ((_ $ (_ $ rel)) :: tl) = prems_of st
-  val measure_trm = 
-    fastype_of rel 
-    |> HOLogic.dest_setT
-    |> mk_size_measure 
-    |> curry (op $) (Const (@{const_name measure}, dummyT))
-    |> Syntax.check_term ctxt
-  val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral 
-    zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals
-in
-  (Function_Relation.relation_tac ctxt measure_trm
-   THEN_ALL_NEW  simp_tac ss) i st
-end
+    val ((_ $ (_ $ rel)) :: tl) = prems_of st
+    val measure_trm = 
+      fastype_of rel 
+      |> HOLogic.dest_setT
+      |> mk_size_measure 
+      |> curry (op $) (Const (@{const_name measure}, dummyT))
+      |> Syntax.check_term ctxt
+    val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral 
+      zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals
+  in
+    (Function_Relation.relation_tac ctxt measure_trm
+     THEN_ALL_NEW  simp_tac ss) i st
+  end
 
 fun prove_termination size_simps ctxt = 
   Function.prove_termination NONE 
@@ -300,24 +300,24 @@
   | map_term' _ _  = NONE;
 
 fun map_thm_tac ctxt tac thm =
-let
-  val monos = Inductive.get_monos ctxt
-  val simps = HOL_basic_ss addsimps @{thms split_def}
-in
-  EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, 
-    REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)),
-    REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
-end
+  let
+    val monos = Inductive.get_monos ctxt
+    val simps = HOL_basic_ss addsimps @{thms split_def}
+  in
+    EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, 
+      REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)),
+      REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
+  end
 
 fun map_thm ctxt f tac thm =
-let
-  val opt_goal_trm = map_term f (prop_of thm)
-in
-  case opt_goal_trm of
-    NONE => thm
-  | SOME goal =>
-     Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) 
-end
+  let
+    val opt_goal_trm = map_term f (prop_of thm)
+  in
+    case opt_goal_trm of
+      NONE => thm
+    | SOME goal =>
+        Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) 
+  end
 
 (*
  inductive premises can be of the form