clarified
authorhaftmann
Tue Oct 30 14:39:36 2007 +0100 (2007-10-30)
changeset 25240ff5815d04c23
parent 25239 3d6abdd10382
child 25241 001ab1d3f567
clarified
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Tue Oct 30 14:39:35 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Oct 30 14:39:36 2007 +0100
     1.3 @@ -176,9 +176,9 @@
     1.4      val legacy_arg = (c', Term.close_schematic_term (Logic.legacy_varify rhs'));
     1.5      val arg = (c', Term.close_schematic_term rhs');
     1.6      (* FIXME workaround based on educated guess *)
     1.7 -    val in_class = is_class andalso c' = NameSpace.qualified (Class.class_prefix target) c;
     1.8 +    val class_global = is_class andalso c' = NameSpace.qualified (Class.class_prefix target) c;
     1.9    in
    1.10 -    not in_class ?
    1.11 +    not class_global ?
    1.12        (Context.mapping_result
    1.13          (Sign.add_abbrev PrintMode.internal pos legacy_arg)
    1.14          (ProofContext.add_abbrev PrintMode.internal pos arg)