src/Pure/Isar/expression.ML
changeset 35625 9c818cab0dd0
parent 35624 c4e29a0bb8c1
child 35798 fd1bb29f8170
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -595,11 +595,11 @@
     1.4  fun atomize_spec thy ts =
     1.5    let
     1.6      val t = Logic.mk_conjunction_balanced ts;
     1.7 -    val body = ObjectLogic.atomize_term thy t;
     1.8 +    val body = Object_Logic.atomize_term thy t;
     1.9      val bodyT = Term.fastype_of body;
    1.10    in
    1.11      if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
    1.12 -    else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
    1.13 +    else (body, bodyT, Object_Logic.atomize (Thm.cterm_of thy t))
    1.14    end;
    1.15  
    1.16  (* achieve plain syntax for locale predicates (without "PROP") *)
    1.17 @@ -634,7 +634,7 @@
    1.18  
    1.19      val args = map Logic.mk_type extraTs @ map Free xs;
    1.20      val head = Term.list_comb (Const (name, predT), args);
    1.21 -    val statement = ObjectLogic.ensure_propT thy head;
    1.22 +    val statement = Object_Logic.ensure_propT thy head;
    1.23  
    1.24      val ([pred_def], defs_thy) =
    1.25        thy