--- a/src/HOL/Tools/choice_specification.ML Mon May 03 16:26:47 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML Mon May 03 20:13:36 2010 +0200
@@ -79,7 +79,7 @@
end
fun add_specification axiomatic cos arg =
- arg |> apsnd Thm.freezeT
+ arg |> apsnd Thm.legacy_freezeT
|> proc_exprop axiomatic cos
|> apsnd Drule.export_without_context
@@ -217,7 +217,7 @@
then writeln "specification"
else ()
in
- arg |> apsnd Thm.freezeT
+ arg |> apsnd Thm.legacy_freezeT
|> process_all (zip3 alt_names rew_imps frees)
end