--- a/Prove.thy	Wed Nov 18 23:52:48 2009 +0100
+++ b/Prove.thy	Thu Nov 19 14:17:10 2009 +0100
@@ -9,7 +9,7 @@
 ML {*
 let
   fun after_qed thm_name thms lthy =
-       LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd
+       Local_Theory.note (thm_name, (flat thms)) lthy |> snd
     
   fun setup_proof (name_spec, (txt, pos)) lthy =
   let