src/Tools/atomize_elim.ML
changeset 35625 9c818cab0dd0
parent 33040 cffdb7b28498
child 41228 e1fce873b814
     1.1 --- a/src/Tools/atomize_elim.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/Tools/atomize_elim.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -59,9 +59,9 @@
     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 ObjectLogic.atomize_prems)) ctxt
     1.8 +    (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt
     1.9      then_conv MetaSimplifier.rewrite true (AtomizeElimData.get ctxt)
    1.10 -    then_conv (fn ct' => if can ObjectLogic.dest_judgment ct'
    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])))
    1.14      ct