--- a/ProgTutorial/Base.thy	Wed Nov 18 14:06:01 2009 +0100
+++ b/ProgTutorial/Base.thy	Thu Nov 19 14:11:50 2009 +0100
@@ -5,6 +5,10 @@
   ("antiquote_setup.ML")
 begin
 
+notation (latex output)
+  Cons ("_ # _" [66,65] 65)
+
+
 (* rebinding of writeln and tracing so that it can *)
 (* be compared in intiquotations                   *)
 ML {* 
@@ -86,7 +90,7 @@
 
 ML {*
 fun propagate_env (context as Context.Proof lthy) =
-      Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
+      Context.Proof (Local_Theory.map_contexts (ML_Env.inherit context) lthy)
   | propagate_env context = context
 
 fun propagate_env_prf prf = Proof.map_contexts