diff -r 486d4647bb37 -r 8f8652a8107f Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Fri Sep 10 09:17:40 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Sat Sep 11 05:56:49 2010 +0800
@@ -29,63 +29,63 @@
 
 (* defines the quotient types *)
 fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =
-let
-  val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms
-  val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms
-in
-  fold_map Quotient_Type.add_quotient_type qty_args2 lthy
-end 
+  let
+    val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms
+    val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms
+  in
+    fold_map Quotient_Type.add_quotient_type qty_args2 lthy
+  end 
 
 
 (* defines quotient constants *)
 fun define_qconsts qtys consts_specs lthy =
-let
-  val (qconst_infos, lthy') = 
-    fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy
-  val phi = ProofContext.export_morphism lthy' lthy
-in
-  (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy')
-end
+  let
+    val (qconst_infos, lthy') = 
+      fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy
+    val phi = ProofContext.export_morphism lthy' lthy
+  in
+    (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy')
+  end
 
 
 (* defines the quotient permutations and proves pt-class *)
 fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy =
-let
-  val lthy1 = 
-    lthy
-    |> Local_Theory.exit_global
-    |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) 
+  let
+    val lthy1 = 
+      lthy
+      |> Local_Theory.exit_global
+      |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) 
   
-  val (qs, lthy2) = define_qconsts qtys perm_specs lthy1
+    val (qs, lthy2) = define_qconsts qtys perm_specs lthy1
 
-  val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2
+    val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2
 
-  val lifted_perm_laws = 
-    map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws'
-    |> Variable.exportT lthy3 lthy2
+    val lifted_perm_laws = 
+      map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws'
+      |> Variable.exportT lthy3 lthy2
 
-  fun tac _ =
-    Class.intro_classes_tac [] THEN
-      (ALLGOALS (resolve_tac lifted_perm_laws))
-in
-  lthy2
-  |> Class.prove_instantiation_exit tac 
-  |> Named_Target.theory_init
-end
+    fun tac _ =
+      Class.intro_classes_tac [] THEN
+        (ALLGOALS (resolve_tac lifted_perm_laws))
+  in
+    lthy2
+    |> Class.prove_instantiation_exit tac 
+    |> Named_Target.theory_init
+  end
 
 
 (* defines the size functions and proves size-class *)
 fun define_qsizes qtys qfull_ty_names tvs size_specs lthy =
-let
-  fun tac _ = Class.intro_classes_tac []
-in
-  lthy
-  |> Local_Theory.exit_global
-  |> Class.instantiation (qfull_ty_names, tvs, @{sort size})
-  |> snd o (define_qconsts qtys size_specs)
-  |> Class.prove_instantiation_exit tac
-  |> Named_Target.theory_init
-end
+  let
+    val tac = K (Class.intro_classes_tac [])
+  in
+    lthy
+    |> Local_Theory.exit_global
+    |> Class.instantiation (qfull_ty_names, tvs, @{sort size})
+    |> snd o (define_qconsts qtys size_specs)
+    |> Class.prove_instantiation_exit tac
+    |> Named_Target.theory_init
+  end
 
 
 (* lifts a theorem and cleans all "_raw" parts
@@ -99,28 +99,28 @@
   val parser = Scan.repeat (exclude || any)
 in
   fun unraw_str s =
-   s |> explode
-     |> Scan.finite Symbol.stopper parser >> implode 
-     |> fst
+    s |> explode
+      |> Scan.finite Symbol.stopper parser >> implode 
+      |> fst
 end
 
 fun unraw_vars_thm thm =
-let
-  fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)
+  let
+    fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)
 
-  val vars = Term.add_vars (prop_of thm) []
-  val vars' = map (Var o unraw_var_str) vars
-in
-  Thm.certify_instantiate ([], (vars ~~ vars')) thm
-end
+    val vars = Term.add_vars (prop_of thm) []
+    val vars' = map (Var o unraw_var_str) vars
+  in
+    Thm.certify_instantiate ([], (vars ~~ vars')) thm
+  end
 
 fun unraw_bounds_thm th =
-let
-  val trm = Thm.prop_of th
-  val trm' = Term.map_abs_vars unraw_str trm
-in
-  Thm.rename_boundvars trm trm' th
-end
+  let
+    val trm = Thm.prop_of th
+    val trm' = Term.map_abs_vars unraw_str trm
+  in
+    Thm.rename_boundvars trm trm' th
+  end
 
 fun lift_thms qtys simps thms ctxt =
   (map (Quotient_Tacs.lifted ctxt qtys simps