src/HOL/Tools/Quotient/quotient_tacs.ML
changeset 35625 9c818cab0dd0
parent 35222 4f1fba00f66d
child 35788 f1deaca15ca3
     1.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -48,7 +48,7 @@
     1.4  fun atomize_thm thm =
     1.5  let
     1.6    val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
     1.7 -  val thm'' = ObjectLogic.atomize (cprop_of thm')
     1.8 +  val thm'' = Object_Logic.atomize (cprop_of thm')
     1.9  in
    1.10    @{thm equal_elim_rule1} OF [thm'', thm']
    1.11  end
    1.12 @@ -616,7 +616,7 @@
    1.13  
    1.14  (* the tactic leaves three subgoals to be proved *)
    1.15  fun procedure_tac ctxt rthm =
    1.16 -  ObjectLogic.full_atomize_tac
    1.17 +  Object_Logic.full_atomize_tac
    1.18    THEN' gen_frees_tac ctxt
    1.19    THEN' SUBGOAL (fn (goal, i) =>
    1.20      let