--- a/ProgTutorial/General.thy	Thu Nov 05 10:30:59 2009 +0100
+++ b/ProgTutorial/General.thy	Sat Nov 07 01:03:37 2009 +0100
@@ -174,15 +174,87 @@
 text {*
   Like with terms, there is the distinction between free type
   variables (term-constructor @{ML "TFree"}) and schematic
-  type variables (term-constructor @{ML "TVar"}). A type constant,
+  type variables (term-constructor @{ML "TVar"} and printed with
+  a leading question mark). A type constant,
   like @{typ "int"} or @{typ bool}, are types with an empty list
-  of argument types. However, it is a bit difficult to show an
-  example, because Isabelle always pretty-prints types (unlike terms).
-  Here is a contrived example:
+  of argument types. However, it needs a bit of effort to show an
+  example, because Isabelle always pretty prints types (unlike terms).
+  Using just the antiquotation @{text "@{typ \"bool\"}"} we only see
 
   @{ML_response [display, gray]
-  "if Type (\"bool\", []) = @{typ \"bool\"} then true else false"
-  "true"}
+  "@{typ \"bool\"}"
+  "bool"}
+
+  the pretty printed version of @{text "bool"}. However, in PolyML it is 
+  easy to install your own pretty printer. With the function below we 
+  mimic the behaviour of the usual pretty printer for 
+  datatypes.\footnote{Thanks to David Matthews for providing this
+  code.}
+*}
+
+ML{*fun typ_raw_pretty_printer depth _ ty =
+let
+ fun cond str a =
+   if depth <= 0 
+   then PolyML.PrettyString "..."
+   else PolyML.PrettyBlock(1, false, [], 
+          [PolyML.PrettyString str, PolyML.PrettyBreak(1, 0), a])
+in 
+  case ty of
+    Type a  => cond "Type"  (PolyML.prettyRepresentation(a, depth - 1))
+  | TFree a => cond "TFree" (PolyML.prettyRepresentation(a, depth - 1)) 
+  | TVar a  => cond "TVar"  (PolyML.prettyRepresentation(a, depth - 1))
+end*}
+
+text {*
+  We can install this pretty printer with the function 
+  @{ML_ind addPrettyPrinter in PolyML} as follows.
+*}
+
+ML{*PolyML.addPrettyPrinter typ_raw_pretty_printer*}
+
+text {*
+  Now the type bool is printed out as expected.
+
+  @{ML_response [display,gray]
+  "@{typ \"bool\"}"
+  "Type (\"bool\", [])"}
+
+  When printing out a list-type
+  
+  @{ML_response [display,gray]
+  "@{typ \"'a list\"}"
+  "Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"}
+
+  we can see the full name of the type is actually @{text "List.list"}, indicating
+  that it is defined in the theory @{text "List"}. However, one has to be 
+  careful with finding out the right name of a type, because even if
+  @{text "fun"}, @{text "bool"} and @{text "nat"} are defined in the 
+  theories @{text "HOL"} and @{text "Nat"}, respectively, they are 
+  still represented by their simple name.
+
+   @{ML_response [display,gray]
+  "@{typ \"bool \<Rightarrow> nat\"}"
+  "Type (\"fun\", [Type (\"bool\", []), Type (\"nat\", [])])"}
+
+  We can restore the usual behaviour of Isabelle's pretty printer
+  with the code
+*}
+
+ML{*fun stnd_pretty_printer _ _ =   
+  ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy;
+
+PolyML.addPrettyPrinter stnd_pretty_printer*}
+
+text {*
+  After that the types for booleans, lists and so on are printed out again 
+  the standard Isabelle way.
+
+  @{ML_response_fake [display, gray]
+  "@{typ \"bool\"};
+@{typ \"'a list\"}"
+  "\"bool\"
+\"'a List.list\""}
 
   \begin{readmore}
   Types are described in detail in \isccite{sec:types}. Their
@@ -1119,14 +1191,14 @@
 
   consisting of a name and a kind.  When we store lemmas in the theorem database, 
   we might want to explicitly extend this data by attaching case names to the 
-  two premises of the lemma.  This can be done with the function @{ML_ind name in RuleCases}
-  from the structure @{ML_struct RuleCases}.
+  two premises of the lemma.  This can be done with the function @{ML_ind name in Rule_Cases}
+  from the structure @{ML_struct Rule_Cases}.
 *}
 
 local_setup %gray {*
   LocalTheory.note Thm.lemmaK
     ((@{binding "foo_data'"}, []), 
-      [(RuleCases.name ["foo_case_one", "foo_case_two"] 
+      [(Rule_Cases.name ["foo_case_one", "foo_case_two"] 
         @{thm foo_data})]) #> snd *}
 
 text {*