# HG changeset patch
# User paulson
# Date 861611926 -7200
# Node ID 8f89a99d2b009cc1ded6b18e54829cb023810277
# Parent  7ecb8b6a3d7fefbca975f899c1de58923bf349af
Tidied up the indentation

diff -r 7ecb8b6a3d7f -r 8f89a99d2b00 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Mon Apr 21 10:16:41 1997 +0200
+++ b/src/HOL/Lambda/ParRed.thy	Mon Apr 21 10:38:46 1997 +0200
@@ -28,10 +28,9 @@
 
 primrec cd dB
   "cd(Var n) = Var n"
-  "cd(s @ t) = (case s of
-            Var n => s @ (cd t) |
-            s1 @ s2 => (cd s) @ (cd t) |
-            Abs u => deAbs(cd s)[cd t/0])"
+  "cd(s @ t) = (case s of Var n   => (s @ cd t)
+                        | s1 @ s2 => (cd s @ cd t) 
+                        | Abs u   => deAbs(cd s)[cd t/0])"
   "cd(Abs s) = Abs(cd s)"
 
 primrec deAbs dB