src/HOL/Tools/specification_package.ML
changeset 22578 b0eb5652f210
parent 22101 6d13239d5f52
child 22709 9ab51bac6287
--- a/src/HOL/Tools/specification_package.ML	Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Tools/specification_package.ML	Wed Apr 04 00:11:03 2007 +0200
@@ -32,7 +32,7 @@
             Const("Ex",_) $ P =>
             let
                 val ctype = domain_type (type_of P)
-                val cname_full = Sign.intern_const (sign_of thy) cname
+                val cname_full = Sign.intern_const thy cname
                 val cdefname = if thname = ""
                                then Thm.def_name (Sign.base_name cname)
                                else thname
@@ -58,7 +58,7 @@
                     Const("Ex",_) $ P =>
                     let
                         val ctype = domain_type (type_of P)
-                        val cname_full = Sign.intern_const (sign_of thy) cname
+                        val cname_full = Sign.intern_const thy cname
                         val cdefname = if thname = ""
                                        then Thm.def_name (Sign.base_name cname)
                                        else thname
@@ -183,7 +183,8 @@
                     in
                         thm RS spec'
                     end
-                fun remove_alls frees thm = Library.foldl (inst_all (sign_of_thm thm)) (thm,frees)
+                fun remove_alls frees thm =
+                    Library.foldl (inst_all (Thm.theory_of_thm thm)) (thm,frees)
                 fun process_single ((name,atts),rew_imp,frees) args =
                     let
                         fun undo_imps thm =