diff -r a0b280dd4bc7 -r 520127b708e6 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Tue Jul 20 13:34:44 2010 +0100
+++ b/ProgTutorial/Essential.thy	Wed Jul 28 19:09:49 2010 +0200
@@ -1,12 +1,12 @@
 theory Essential
-imports Base FirstSteps
+imports Base First_Steps
 begin
 
 (*<*)
 setup{*
 open_file_with_prelude 
   "Essential_Code.thy"
-  ["theory Essential", "imports Base FirstSteps", "begin"]
+  ["theory Essential", "imports Base First_Steps", "begin"]
 *}
 (*>*)
 
@@ -84,8 +84,8 @@
   val v2 = Var ((\"x1\", 3), @{typ bool})
   val v3 = Free (\"x\", @{typ bool})
 in
-  string_of_terms @{context} [v1, v2, v3]
-  |> tracing
+  pretty_terms @{context} [v1, v2, v3]
+  |> pwriteln
 end"
 "?x3, ?x1.3, x"}
 
@@ -118,7 +118,7 @@
 "let
   val omega = Free (\"x\", @{typ \"nat \<Rightarrow> nat\"}) $ Free (\"x\", @{typ nat})
 in 
-  tracing (string_of_term @{context} omega)
+  pwriteln (pretty_term @{context} omega)
 end"
   "x x"}
   
@@ -423,8 +423,8 @@
   val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}
 in 
   subst_bounds (rev vrs, trm) 
-  |> string_of_term @{context}
-  |> tracing
+  |> pretty_term @{context}
+  |> pwriteln
 end"
   "x = y"}
 
@@ -457,8 +457,8 @@
 "let
   val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
 in
-  string_of_term @{context} eq
-  |> tracing
+  eq |> pretty_term @{context}
+     |> pwriteln
 end"
   "True = False"}
 
@@ -713,15 +713,15 @@
   \begin{isabelle}*}
 ML{*fun pretty_helper aux env =
   env |> Vartab.dest  
-      |> map ((fn (s1, s2) => s1 ^ " := " ^ s2) o aux) 
-      |> commas 
-      |> enclose "[" "]" 
-      |> tracing
+      |> map ((fn (s1, s2) => Pretty.block [s1, Pretty.str ";=", s2]) o aux) 
+      |> Pretty.commas 
+      |> Pretty.enum "" "[" "]" 
+      |> pwriteln
 
 fun pretty_tyenv ctxt tyenv =
 let
   fun get_typs (v, (s, T)) = (TVar (v, s), T)
-  val print = pairself (Syntax.string_of_typ ctxt)
+  val print = pairself (pretty_typ ctxt)
 in 
   pretty_helper (print o get_typs) tyenv
 end*}
@@ -901,7 +901,7 @@
 ML{*fun pretty_env ctxt env =
 let
   fun get_trms (v, (T, t)) = (Var (v, T), t) 
-  val print = pairself (string_of_term ctxt)
+  val print = pairself (pretty_term ctxt)
 in
   pretty_helper (print o get_trms) env 
 end*}
@@ -942,8 +942,8 @@
   val trm = @{term_pat \"(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y\"}
 in
   Envir.subst_term (Vartab.empty, fo_env) trm
-  |> string_of_term @{context}
-  |> tracing
+  |> pretty_term @{context}
+  |> pwriteln
 end"
   "P (\<lambda>a b. Q b a)"}
 
@@ -1024,106 +1024,6 @@
   "Envir.type_env"}. An assumption of this function is that the terms to be
   unified have already the same type. In case of failure, the exceptions that
   are raised are either @{text Pattern}, @{text MATCH} or @{text Unif}.
-*}
-
-(*
-ML {*
-  fun patunif_in_emptyenv (t, u) =
-    let
-      val init = Envir.empty 0;
-      val env = Pattern.unify @{theory} (t, u) init;
-    in
-      (env |> Envir.term_env |> Vartab.dest,
-       env |> Envir.type_env |> Vartab.dest)
-    end
-*}
-
-text {*
-@{ML_response [display, gray]
- "val t1 = @{term_pat \"(% x y. ?f y x)\"};
- val u1 = @{term_pat \"z::bool\"};
-   (* type conflict isnt noticed *)
- patunif_in_emptyenv (t1, u1);"
- "check missing"
-*}
-@{ML_response [display, gray] 
- "val t2 = @{term_pat \"(% y. ?f y)\"} |> Term.strip_abs_body;
- val u2 = @{term_pat \"z::bool\"};
-   (* fails because of loose bounds *)
- (* patunif_in_emptyenv (t2, u2) *)"
- "check missing"
-*}
-@{ML_response [display, gray]
- "val t3 = @{term_pat \"(% y. plu (?f y) (% x. g x))\"};
- val u3 = @{term_pat \"(% y. plu y (% x. g x))\"};
-   (* eta redexe im term egal, hidden polym wird inst *)
- patunif_in_emptyenv (t3, u3)"
- "check missing"
-*}
-@{ML_response [display, gray] 
- "val t4 = @{term_pat \"(% y. plu (?f y) ((% x. g x) k))\"};
- val u4 = @{term_pat \"(% y. plu y ((% x. g x) k))\"};
-   (* beta redexe are largely ignored, hidden polymorphism is instantiated *)
- patunif_in_emptyenv (t4, u4)"
- "check missing"
-*}
-@{ML_response [display, gray]
- "val t5 = @{term_pat \"(% y. plu ((% x. ?f) y) ((% x. g x) k))\"};
- val u5 = @{term_pat \"(% y. plu y ((% x. g x) k))\"};
-   (* fails: can't have beta redexes which seperate a var from its arguments *)
- (* patunif_in_emptyenv (t5, u5) *)"
-*}
-
-@{ML_response [display, gray] 
- "val t6 = @{term_pat \"(% x y. ?f x y) a b\"};
- val u6 = @{term_pat \"c\"};
- (* Pattern.pattern assumes argument is beta-normal *)
- Pattern.pattern t6; 
-   (* fails: can't have beta redexes which seperate a var from its arguments,
-       otherwise this would be general unification for general a,b,c *)
- (* patunif_in_emptyenv (t6, u6) *)"
-*}
-@{ML_response [display, gray]
- "val t7 = @{term_pat \"(% y. plu ((% x. ?f x) y) ((% x. g x) k))\"};
- val u7 = @{term_pat \"(% y. plu y ((% x. g x) k))\"};
-   (* eta redexe die Pattern trennen brauchen nicht normalisiert sein *)
- patunif_in_emptyenv (t7, u7)"
-*}
-@{ML_response [display, gray] 
- "val t8 = @{term_pat \"(% y. ?f y)\"};
- val u8 = @{term_pat \"(% y. y ?f)\"};
-   (* variables of the same name are identified *)
- (* patunif_in_emptyenv (t8, u8) *)"
-*}
-
-@{ML_response [display, gray]
- "val t9 = @{term_pat \"(% y. ?f y)\"};
- val u9 = @{term_pat \"(% y. ?f y)\"};
-   (* trivial solutions are empty and don't contain ?f = ?f etc *)
- patunif_in_emptyenv (t9, u9)"
-*}
-@{ML_response [display, gray] 
- "val t10 = @{term_pat \"(% y. (% x. ?f x) y)\"};
- val u10 = @{term_pat \"(% y. ?f y)\"};
-   (* trivial solutions are empty and don't contain ?f = ?f etc *)
- patunif_in_emptyenv (t10, u10)"
-*}
-@{ML_response [display, gray]
- "val t11 = @{term_pat \"(% z. ?f z)\"};
- val u11 = @{term_pat \"(% z. k (?f z))\"};
-   (* fails: occurs check *)
- (* patunif_in_emptyenv (t11, u11) *)"
-*}
-@{ML_response [display, gray]
- "val t12 = @{term_pat \"(% z. ?f z)\"};
- val u12 = @{term_pat \"?g a\"};
-   (* fails: *both* terme have to be higher-order patterns *)
- (* patunif_in_emptyenv (t12, u12) *)"
-*}
-*}
-*)
-
-text {*
 
   As mentioned before, unrestricted higher-order unification, respectively
   unrestricted higher-order matching, is in general undecidable and might also
@@ -1719,7 +1619,7 @@
   val eq = @{thm True_def}
 in
   (Thm.lhs_of eq, Thm.rhs_of eq) 
-  |> pairself (string_of_cterm @{context})
+  |> pairself (Pretty.string_of o (pretty_cterm @{context}))
 end"
   "(True, (\<lambda>x. x) = (\<lambda>x. x))"}
 
@@ -1738,10 +1638,11 @@
 "let
   val ctxt = @{context}
   fun prems_and_concl thm =
-     [\"Premises: \"   ^ (string_of_terms ctxt (Thm.prems_of thm))] @ 
-     [\"Conclusion: \" ^ (string_of_term ctxt (Thm.concl_of thm))]
-     |> cat_lines
-     |> tracing
+     [[Pretty.str \"Premises:\", pretty_terms ctxt (Thm.prems_of thm)], 
+      [Pretty.str \"Conclusion:\", pretty_term ctxt (Thm.concl_of thm)]]
+     |> map Pretty.block
+     |> Pretty.chunks
+     |> pwriteln
 in
   prems_and_concl @{thm foo_test1};
   prems_and_concl @{thm foo_test2}