--- a/CookBook/FirstSteps.thy	Wed Jan 14 16:46:07 2009 +0000
+++ b/CookBook/FirstSteps.thy	Wed Jan 14 17:47:49 2009 +0000
@@ -93,8 +93,7 @@
   amounts of trace output. This redirection can be achieved using the code
 *}
 
-ML{* 
-val strip_specials =
+ML{*val strip_specials =
 let
   fun strip ("\^A" :: _ :: cs) = strip cs
     | strip (c :: cs) = c :: strip cs
@@ -105,8 +104,7 @@
  Output.tracing_fn := (fn s =>
     (TextIO.output (stream, (strip_specials s));
      TextIO.output (stream, "\n");
-     TextIO.flushOut stream)); 
-*}
+     TextIO.flushOut stream)) *}
 
 text {*
 
@@ -137,9 +135,7 @@
   determined at ``compile-time'', not ``run-time''. For example the function
 *}
 
-ML {*
-fun not_current_thyname () = Context.theory_name @{theory}
-*}
+ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
 
 text {*
 
@@ -163,9 +159,7 @@
   avoid explicit bindings for theorems such as
 *}
 
-ML {*
-val allI = thm "allI"
-*}
+ML{*val allI = thm "allI" *}
 
 text {*
   These bindings were difficult to maintain and also could accidentally
@@ -261,13 +255,11 @@
   as arguments can only be written as
 *}
 
-ML {*
-fun make_imp P Q tau =
+ML{*fun make_imp P Q tau =
   let
     val x = Free ("x",tau)
   in Logic.all x (Logic.mk_implies (P $ x, Q $ x))
-  end
-*}
+  end *}
 
 text {*
 
@@ -275,9 +267,7 @@
   @{term "tau"} into an antiquotation. For example the following does \emph{not} work:
 *}
 
-ML {*
-fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 
-*}
+ML{*fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} *}
 
 text {*
   To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 
@@ -323,17 +313,13 @@
 
 *} 
 
-ML {*
-fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2])
-*}
+ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}
 
 text {*
   which can be equally written as 
 *}
 
-ML {*
-fun make_fun_type tau1 tau2 = tau1 --> tau2
-*}
+ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
 
 text {*