src/Pure/Isar/element.ML
changeset 35625 9c818cab0dd0
parent 35624 c4e29a0bb8c1
child 35767 086504a943af
     1.1 --- a/src/Pure/Isar/element.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -223,12 +223,12 @@
     1.4      val cert = Thm.cterm_of thy;
     1.5  
     1.6      val th = MetaSimplifier.norm_hhf raw_th;
     1.7 -    val is_elim = ObjectLogic.is_elim th;
     1.8 +    val is_elim = Object_Logic.is_elim th;
     1.9  
    1.10      val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false ctxt);
    1.11      val prop = Thm.prop_of th';
    1.12      val (prems, concl) = Logic.strip_horn prop;
    1.13 -    val concl_term = ObjectLogic.drop_judgment thy concl;
    1.14 +    val concl_term = Object_Logic.drop_judgment thy concl;
    1.15  
    1.16      val fixes = fold_aterms (fn v as Free (x, T) =>
    1.17          if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)