--- a/src/HOL/Tools/choice_specification.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Tools/choice_specification.ML Sat Oct 17 00:52:37 2009 +0200
@@ -75,7 +75,7 @@
fun add_specification axiomatic cos arg =
arg |> apsnd Thm.freezeT
|> proc_exprop axiomatic cos
- |> apsnd standard
+ |> apsnd Drule.standard
(* Collect all intances of constants in term *)
@@ -188,7 +188,7 @@
in
args |> apsnd (remove_alls frees)
|> apsnd undo_imps
- |> apsnd standard
+ |> apsnd Drule.standard
|> Thm.theory_attributes (map (Attrib.attribute thy) atts)
|> add_final
|> Library.swap