# HG changeset patch
# User paulson
# Date 858694262 -3600
# Node ID 6e5b2d6503ebde57e6e21eaef1db5e9f95de0e78
# Parent  889d99613720c7999410303da7e10d4ad841ca92
Made the indentation rational

diff -r 889d99613720 -r 6e5b2d6503eb src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Mar 18 14:35:10 1997 +0100
+++ b/src/HOL/simpdata.ML	Tue Mar 18 15:11:02 1997 +0100
@@ -364,17 +364,20 @@
 
 (* rot_eq_tac rotates the first equality premise of subgoal i to the front,
    fails if there is no equaliy or if an equality is already at the front *)
-fun rot_eq_tac i = let
-  fun is_eq (Const ("Trueprop", _) $ (Const("op =",_) $ _ $ _)) = true
-  |   is_eq _ = false;
-  fun find_eq n [] = None
-  |   find_eq n (t :: ts) = if (is_eq t) then Some n else find_eq (n + 1) ts;
-  fun rot_eq state = let val (_, _, Bi, _) = dest_state (state, i) in
-	    (case find_eq 0 (Logic.strip_assums_hyp Bi) of
-	      None   => no_tac
-	    | Some 0 => no_tac
-	    | Some n => rotate_tac n i) end;
-in STATE rot_eq end;
+fun rot_eq_tac i = 
+  let fun is_eq (Const ("Trueprop", _) $ (Const("op =",_) $ _ $ _)) = true
+	| is_eq _ = false;
+      fun find_eq n [] = None
+	| find_eq n (t :: ts) = if (is_eq t) then Some n 
+				else find_eq (n + 1) ts;
+      fun rot_eq state = 
+	  let val (_, _, Bi, _) = dest_state (state, i) 
+	  in  case find_eq 0 (Logic.strip_assums_hyp Bi) of
+		  None   => no_tac
+		| Some 0 => no_tac
+		| Some n => rotate_tac n i
+	  end;
+  in STATE rot_eq end;
 
 (*an unsatisfactory fix for the incomplete asm_full_simp_tac!
   better: asm_really_full_simp_tac, a yet to be implemented version of
@@ -423,10 +426,12 @@
 fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
 fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
 
-fun auto_tac (cs,ss) = let val cs' = cs addss ss in
-EVERY [	TRY (safe_tac cs'),
-	REPEAT (FIRSTGOAL (fast_tac cs')),
-	prune_params_tac] end;
+fun auto_tac (cs,ss) = 
+    let val cs' = cs addss ss 
+    in  EVERY [TRY (safe_tac cs'),
+	       REPEAT (FIRSTGOAL (fast_tac cs')),
+	       prune_params_tac] 
+    end;
 
 fun Auto_tac () = auto_tac (!claset, !simpset);