--- a/ProgTutorial/Base.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Base.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -12,117 +12,6 @@
 notation (latex output)
   Cons ("_ # _" [66,65] 65)
 
-
-(* re-definition of various ML antiquotations     *)
-(* to have a special tag for text enclosed in ML; *)
-(* they also write the code into a separate file  *)
-
-ML {*
-val filename = Attrib.setup_config_string @{binding "filename"} (K "File_Code.ML")
-*}
-
-
-ML {*
-fun write_file txt thy =
-let 
-  val stream = Config.get_global thy filename
-               |> TextIO.openAppend 
-in
-  TextIO.output (stream, txt); 
-  TextIO.flushOut stream;       (* needed ?*)
-  TextIO.closeOut stream
-end
-*}
-
-ML {*
-fun write_file_ml_blk txt thy =
-let
-  val pre  = implode ["\n", "ML ", "{", "*", "\n"]
-  val post = implode ["\n", "*", "}", "\n"]
-  val _ = write_file (enclose pre post txt) thy
-in
-  thy
-end
-
-fun write_file_setup_blk txt thy =
-let
-  val pre  = implode ["\n", "setup ", "{", "*", "\n"]
-  val post = implode ["\n", "*", "}", "\n"]
-  val _ = write_file (enclose pre post txt) thy
-in
-  thy
-end
-
-fun write_file_lsetup_blk txt lthy =
-let
-  val pre  = implode ["\n", "local_setup ", "{", "*", "\n"]
-  val post = implode ["\n", "*", "}", "\n"]
-  val _ = write_file (enclose pre post txt) (Proof_Context.theory_of lthy)
-in
-  lthy
-end
-
-*}
-
-ML {*
-fun open_file name thy =
-let  
-  val _ = tracing ("Open File: " ^ name)
-  val _ = TextIO.openOut name
-in 
-  Config.put_global filename name thy
-end
-*}
-
-ML {*
-fun open_file_with_prelude name txts thy =
-let 
-  val thy' = open_file name thy 
-  val _ = write_file (cat_lines txts) thy'
-in
-  thy'
-end
-*}
-
-ML {*
-val _ =
-  Outer_Syntax.command ("ML", Keyword.tag "TutorialML" Keyword.thy_decl)
-    "ML text within theory or local theory"
-    (Parse.ML_source >> (fn (txt, pos) =>
-      Toplevel.generic_theory
-        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
-          Local_Theory.propagate_ml_env #> Context.map_theory (write_file_ml_blk txt))))
-*}
-
-ML {*
-val _ =
-  Outer_Syntax.command ("ML_prf", Keyword.tag "TutorialMLprf" Keyword.prf_decl) "ML text within proof"
-    (Parse.ML_source >> (fn (txt, pos) =>
-      Toplevel.proof (Proof.map_context (Context.proof_map
-        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));
-*}
-
-
-ML {*
-val _ =
-  Outer_Syntax.command ("ML_val", Keyword.tag "TutorialML" Keyword.diag) "diagnostic ML text" 
-    (Parse.ML_source >> Isar_Cmd.ml_diag true)
-*}
-
-ML {*
-val _ =
-  Outer_Syntax.command ("setup", Keyword.tag_ml Keyword.thy_decl) "ML theory setup" 
-      (Parse.ML_source >> (fn (txt, pos) => 
-        (Toplevel.theory (Isar_Cmd.global_setup (txt, pos) #> write_file_setup_blk txt))))
-*}
-
-ML {*
-val _ =
-  Outer_Syntax.local_theory ("local_setup", Keyword.tag_ml Keyword.thy_decl) "ML local theory setup" 
-      (Parse.ML_source >> (fn (txt, pos) => 
-         Isar_Cmd.local_setup (txt, pos) #> write_file_lsetup_blk txt));
-*}
-
 ML {*
 fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n)