--- a/Nominal-General/nominal_permeq.ML	Sat Sep 11 05:56:49 2010 +0800
+++ b/Nominal-General/nominal_permeq.ML	Sun Sep 12 22:46:40 2010 +0800
@@ -41,33 +41,33 @@
 fun trace_enabled ctxt = Config.get ctxt trace_eqvt
 
 fun trace_msg ctxt result = 
-let
-  val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result))
-  val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result))
-in
-  warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str]))
-end
+  let
+    val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result))
+    val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result))
+  in
+    warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str]))
+  end
 
 fun trace_conv ctxt conv ctrm =
-let
-  val result = conv ctrm
-in
-  if Thm.is_reflexive result 
-  then result
-  else (trace_msg ctxt result; result)
-end
+  let
+    val result = conv ctrm
+  in
+    if Thm.is_reflexive result 
+    then result
+    else (trace_msg ctxt result; result)
+  end
 
 (* this conversion always fails, but prints 
    out the analysed term  *)
 fun trace_info_conv ctxt ctrm = 
-let
-  val trm = term_of ctrm
-  val _ = case (head_of trm) of 
-      @{const "Trueprop"} => ()
-    | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm)
-in
-  Conv.no_conv ctrm
-end
+  let
+    val trm = term_of ctrm
+    val _ = case (head_of trm) of 
+        @{const "Trueprop"} => ()
+      | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm)
+  in
+    Conv.no_conv ctrm
+  end
 
 (* conversion for applications *)
 fun eqvt_apply_conv ctrm =
@@ -101,39 +101,39 @@
   | is_excluded _ _ = false 
 
 fun progress_info_conv ctxt strict_flag excluded ctrm =
-let
-  fun msg trm =
-    if is_excluded excluded trm then () else 
-      (if strict_flag then error else warning) 
-        ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
+  let
+    fun msg trm =
+      if is_excluded excluded trm then () else 
+        (if strict_flag then error else warning) 
+          ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
 
-  val _ = case (term_of ctrm) of
-      Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm
-    | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm
-    | _ => () 
-in
-  Conv.all_conv ctrm 
-end
+    val _ = case (term_of ctrm) of
+        Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm
+      | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm
+      | _ => () 
+  in
+    Conv.all_conv ctrm 
+  end
 
 (* main conversion *) 
 fun eqvt_conv ctxt strict_flag user_thms excluded ctrm =
-let
-  val first_conv_wrapper = 
-    if trace_enabled ctxt 
-    then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt))
-    else Conv.first_conv
+  let
+    val first_conv_wrapper = 
+      if trace_enabled ctxt 
+      then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt))
+      else Conv.first_conv
 
-  val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt
-  val post_thms = map safe_mk_equiv @{thms permute_pure}
-in
-  first_conv_wrapper
-    [ Conv.rewrs_conv pre_thms,
-      eqvt_apply_conv,
-      eqvt_lambda_conv,
-      Conv.rewrs_conv post_thms,
-      progress_info_conv ctxt strict_flag excluded
-    ] ctrm
-end
+    val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt
+    val post_thms = map safe_mk_equiv @{thms permute_pure}
+  in
+    first_conv_wrapper
+      [ Conv.rewrs_conv pre_thms,
+        eqvt_apply_conv,
+        eqvt_lambda_conv,
+        Conv.rewrs_conv post_thms,
+        progress_info_conv ctxt strict_flag excluded
+      ] ctrm
+  end
 
 (* the eqvt-tactics first eta-normalise goals in 
    order to avoid problems with inductions in the