--- 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) =