
diff -r 718beb785213 -r 06f044466f24 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Fri Oct 30 09:42:16 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Fri Oct 30 09:42:17 2009 +0100
@@ -1134,7 +1134,7 @@
 (
   type T = thm list -> tactic;
   fun init _ = undefined;
-);
+)
 
 val set_tactic = TacticData.put;
 *}




