--- a/src/Provers/simplifier.ML Wed Mar 17 16:33:00 1999 +0100
+++ b/src/Provers/simplifier.ML Wed Mar 17 16:33:47 1999 +0100
@@ -280,13 +280,13 @@
(* access global simpset *)
val simpset_of_sg = ! o simpset_ref_of_sg;
-val simpset_of = simpset_of_sg o sign_of;
+val simpset_of = simpset_of_sg o Theory.sign_of;
-fun SIMPSET tacf state = tacf (simpset_of_sg (sign_of_thm state)) state;
-fun SIMPSET' tacf i state = tacf (simpset_of_sg (sign_of_thm state)) i state;
+fun SIMPSET tacf state = tacf (simpset_of_sg (Thm.sign_of_thm state)) state;
+fun SIMPSET' tacf i state = tacf (simpset_of_sg (Thm.sign_of_thm state)) i state;
val simpset = simpset_of o Context.the_context;
-val simpset_ref = simpset_ref_of_sg o sign_of o Context.the_context;
+val simpset_ref = simpset_ref_of_sg o Theory.sign_of o Context.the_context;
(* change global simpset *)