diff -r 7405ce9d4f25 -r 11d447d5d68c src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Tue Jun 13 23:41:37 2006 +0200
+++ b/src/HOL/Tools/specification_package.ML	Tue Jun 13 23:41:39 2006 +0200
@@ -83,7 +83,7 @@
 end
 
 fun add_specification axiomatic cos arg =
-    arg |> apsnd freezeT
+    arg |> apsnd Thm.freezeT
         |> proc_exprop axiomatic cos
         |> apsnd standard
 
@@ -223,7 +223,7 @@
                         then writeln "specification"
                         else ()
             in
-                arg |> apsnd freezeT
+                arg |> apsnd Thm.freezeT
                     |> process_all (zip3 alt_names rew_imps frees)
             end
             fun post_proc (context, th) =