src/Tools/atomize_elim.ML
changeset 54742 7a86358a3c0b
parent 45294 3c5d3d286055
child 57948 75724d71013c
     1.1 --- a/src/Tools/atomize_elim.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/Tools/atomize_elim.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -59,8 +59,8 @@
     1.4     (EX x y z. ...) | ... | (EX a b c. ...)
     1.5  *)
     1.6  fun atomize_elim_conv ctxt ct =
     1.7 -    (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt
     1.8 -    then_conv Raw_Simplifier.rewrite true (AtomizeElimData.get ctxt)
     1.9 +    (forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt
    1.10 +    then_conv Raw_Simplifier.rewrite ctxt true (AtomizeElimData.get ctxt)
    1.11      then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
    1.12                           then all_conv ct'
    1.13                           else raise CTERM ("atomize_elim", [ct', ct])))