src/HOL/Tools/specification_package.ML
changeset 18799 f137c5e971f5
parent 18776 fdc5379fd359
child 18921 f47c46d7d654
--- a/src/HOL/Tools/specification_package.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/HOL/Tools/specification_package.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -231,7 +231,7 @@
             fun post_proc (context, th) =
                 post_process (Context.theory_of context, th) |>> Context.Theory;
     in
-      IsarThy.theorem_i Drule.internalK
+      IsarThy.theorem_i PureThy.internalK
         ("", [add_spec axiomatic (zip3 names cnames overloaded), post_proc])
         (HOLogic.mk_Trueprop ex_prop, ([], [])) thy
     end