src/HOL/Tools/Qelim/ferrante_rackoff.ML
changeset 35625 9c818cab0dd0
parent 32264 0be31453f698
child 36099 7e1f972df25f
     1.1 --- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -225,9 +225,9 @@
     1.4    (case dlo_instance ctxt p of
     1.5      NONE => no_tac
     1.6    | SOME instance =>
     1.7 -      ObjectLogic.full_atomize_tac i THEN
     1.8 +      Object_Logic.full_atomize_tac i THEN
     1.9        simp_tac (#simpset (snd instance)) i THEN  (* FIXME already part of raw_ferrack_qe_conv? *)
    1.10 -      CONVERSION (ObjectLogic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
    1.11 +      CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
    1.12        simp_tac (simpset_of ctxt) i));  (* FIXME really? *)
    1.13  
    1.14  end;