--- 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; *}