src/HOL/Bali/Basis.thy
changeset 13462 56610e2ba220
parent 12925 99131847fb93
child 13688 a0b16d42d489
     1.1 --- a/src/HOL/Bali/Basis.thy	Tue Aug 06 11:20:47 2002 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Tue Aug 06 11:22:05 2002 +0200
     1.3 @@ -19,11 +19,9 @@
     1.4  
     1.5  declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
     1.6  
     1.7 -(* ###TO HOL/???.ML?? *)
     1.8  ML {*
     1.9 -fun make_simproc name pat pred thm = Simplifier.mk_simproc name
    1.10 -   [Thm.read_cterm (Thm.sign_of_thm thm) (pat, HOLogic.typeT)] 
    1.11 -   (K (K (fn s => if pred s then None else Some (standard (mk_meta_eq thm)))))
    1.12 +fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.sign_of_thm thm) name [pat]
    1.13 +  (fn _ => fn _ => fn t => if pred t then None else Some (mk_meta_eq thm));
    1.14  *}
    1.15  
    1.16  declare split_if_asm  [split] option.split [split] option.split_asm [split]