diff -r da9c26906f3f -r 5d58c100ca3f src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Mar 17 16:32:38 1999 +0100
+++ b/src/Pure/drule.ML	Wed Mar 17 16:33:00 1999 +0100
@@ -305,7 +305,7 @@
   Example is [| ALL x:?A. ?P(x) |] ==> [| ?P(?a) |]
              [ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ]    *)
 fun assume_ax thy sP =
-    let val sign = sign_of thy
+    let val sign = Theory.sign_of thy
         val prop = Logic.close_form (term_of (read_cterm sign (sP, propT)))
     in forall_elim_vars 0 (assume (cterm_of sign prop))  end;
 
@@ -420,7 +420,7 @@
 
 (*** Meta-Rewriting Rules ***)
 
-val proto_sign = sign_of ProtoPure.thy;
+val proto_sign = Theory.sign_of ProtoPure.thy;
 
 fun read_prop s = read_cterm proto_sign (s, propT);