src/HOL/Bali/Basis.thy
changeset 22578 b0eb5652f210
parent 21314 6d709b9bea1a
child 22633 a47e4fd7ebc1
     1.1 --- a/src/HOL/Bali/Basis.thy	Wed Apr 04 00:10:59 2007 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Wed Apr 04 00:11:03 2007 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
     1.5  
     1.6  ML {*
     1.7 -fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.sign_of_thm thm) name [pat]
     1.8 +fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.theory_of_thm thm) name [pat]
     1.9    (fn _ => fn _ => fn t => if pred t then NONE else SOME (mk_meta_eq thm));
    1.10  *}
    1.11