src/Pure/Isar/theory_target.ML
changeset 28793 bb7a102e2f5d
parent 28717 848ffc6b0b8a
child 28822 7ca11ecbc4fb
equal deleted inserted replaced
28792:1d80cee865de 28793:bb7a102e2f5d
   184 
   184 
   185 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((c, mx), rhs) phi =
   185 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((c, mx), rhs) phi =
   186   let
   186   let
   187     val c' = Morphism.name phi c;
   187     val c' = Morphism.name phi c;
   188     val rhs' = Morphism.term phi rhs;
   188     val rhs' = Morphism.term phi rhs;
   189     val name = Name.name_of c;
       
   190     val name' = Name.name_of c';
   189     val name' = Name.name_of c';
   191     val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs'));
   190     val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs'));
   192     val arg = (name', Term.close_schematic_term rhs');
   191     val arg = (name', Term.close_schematic_term rhs');
   193     val similar_body = Type.similar_types (rhs, rhs');
   192     val similar_body = Type.similar_types (rhs, rhs');
   194     (* FIXME workaround based on educated guess *)
   193     (* FIXME workaround based on educated guess *)
   195     val class_global = name = NameSpace.base name'
   194     val class_global = Name.name_of c = Name.name_of c'
   196       andalso Class.class_prefix target = hd (NameSpace.explode name');
   195       andalso not (null (Name.prefix_of c'))
       
   196       andalso (fst o snd o split_last) (Name.prefix_of c') = Class.class_prefix target;
   197   in
   197   in
   198     not (is_class andalso (similar_body orelse class_global)) ?
   198     not (is_class andalso (similar_body orelse class_global)) ?
   199       (Context.mapping_result
   199       (Context.mapping_result
   200         (Sign.add_abbrev PrintMode.internal tags legacy_arg)
   200         (Sign.add_abbrev PrintMode.internal tags legacy_arg)
   201         (ProofContext.add_abbrev PrintMode.internal tags arg)
   201         (ProofContext.add_abbrev PrintMode.internal tags arg)