src/HOL/Bali/Basis.thy

--- a/src/HOL/Bali/Basis.thy	Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Bali/Basis.thy	Wed Apr 04 00:11:03 2007 +0200
@@ -19,7 +19,7 @@
 declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
 
 ML {*
-fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.sign_of_thm thm) name [pat]
+fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.theory_of_thm thm) name [pat]
   (fn _ => fn _ => fn t => if pred t then NONE else SOME (mk_meta_eq thm));
 *}