src/HOL/Tools/Qelim/langford.ML
changeset 35625 9c818cab0dd0
parent 35408 b48ab741683b
child 36945 9bec62c10714
     1.1 --- a/src/HOL/Tools/Qelim/langford.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/Qelim/langford.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -234,11 +234,11 @@
     1.4    (case dlo_instance ctxt p of
     1.5      (ss, NONE) => simp_tac ss i
     1.6    | (ss,  SOME instance) =>
     1.7 -      ObjectLogic.full_atomize_tac i THEN
     1.8 +      Object_Logic.full_atomize_tac i THEN
     1.9        simp_tac ss i
    1.10        THEN (CONVERSION Thm.eta_long_conversion) i
    1.11        THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
    1.12 -      THEN ObjectLogic.full_atomize_tac i
    1.13 -      THEN CONVERSION (ObjectLogic.judgment_conv (raw_dlo_conv ss instance)) i
    1.14 +      THEN Object_Logic.full_atomize_tac i
    1.15 +      THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ss instance)) i
    1.16        THEN (simp_tac ss i)));  
    1.17  end;
    1.18 \ No newline at end of file