--- a/CookBook/FirstSteps.thy	Fri Oct 17 17:41:34 2008 -0400
+++ b/CookBook/FirstSteps.thy	Mon Oct 20 06:22:11 2008 +0000
@@ -133,7 +133,7 @@
   For example, one can print out the name of 
   the current theory by typing
   
-  @{ML_response [display] "Context.theory_name @{theory}" "FirstSteps : string"}
+  @{ML_response [display] "Context.theory_name @{theory}" "FirstSteps"}
  
   where @{text "@{theory}"} is an antiquotation that is substituted with the
   current theory (remember that we assumed we are inside the theory CookBook). 
@@ -338,7 +338,6 @@
 
 *}
 
-
 section {* Type Checking *}
 
 text {* 
@@ -357,13 +356,11 @@
   the @{ML "@{theory}"} antiquotation to get hold of the current theory.
   For example we can write:
 
-  (FIXME ML-response-unchecked needed)
-
-  @{ML [display] "@{term \"(a::nat) + b = c\"}"}
+  @{ML_response_fake [display] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
 
   and 
 
-@{ML [display] 
+@{ML_response_fake [display] 
 "let
   val natT = @{typ \"nat\"}
   val zero = @{term \"0::nat\"}
@@ -371,7 +368,7 @@
   cterm_of @{theory} 
   (Const (@{const_name plus}, natT --> natT --> natT) 
   $ zero $ zero)
-end"}
+end" "0 + 0"}
 
   \begin{exercise}
   Check that the function defined in Exercise~\ref{fun:revsum} returns a
@@ -559,60 +556,6 @@
 
 section {* Theorem Attributes *}
 
-ML {* 
-  val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;
-
-fun ml_val ys txt = "fn " ^
-  (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^
-  " => (" ^ txt ^ ");";
-
-fun ml_val_open (ys, []) txt = ml_val ys txt
-  | ml_val_open (ys, xs) txt =
-      ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end");
-
-fun ml_pat (rhs, pat) =
-  let val pat' = implode (map (fn "\<dots>" => "_" | s => s)
-    (Symbol.explode pat))
-  in
-    "val " ^ pat' ^ " = " ^ rhs
-  end;
-
-(* modified from original *)
-fun ml_val txt = "fn _ => (" ^ txt ^ ");";
-fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;";
-fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
-
-*}
-
-ML {* ml_pat *}
-ML {* K ml_pat *}
-
-ML {*
-fun output_verbatim ml src ctxt (txt, pos) =
-  let val txt = ml ctxt (txt, pos)
-  in
-    (if ! ThyOutput.source then str_of_source src else txt)
-    |> (if ! ThyOutput.quotes then quote else I)
-    |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt
-  end;
-*}
-
-ML {*
-fun output_ml ml = output_verbatim
-  (fn ctxt => fn ((txt, p), pos) =>
-     (ML_Context.eval_in (SOME ctxt) false pos (ml p txt);
-      txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |>
-      Chunks.transform_cmts |> implode));
-*}
-
-ML {* 
-fun output_ml_checked ml src ctxt (txt, pos) =
- (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
- (if ! ThyOutput.source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
-  |> (if ! ThyOutput.quotes then quote else I)
-  |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt)
-
-*}