--- a/src/Pure/Isar/theory_target.ML Mon Aug 09 15:19:45 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML Mon Aug 09 15:20:50 2010 +0200
@@ -195,6 +195,33 @@
end;
+(* consts in locales *)
+
+fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
+ let
+ val b' = Morphism.binding phi b;
+ val rhs' = Morphism.term phi rhs;
+ val arg = (b', Term.close_schematic_term rhs');
+ val same_shape = Term.aconv_untyped (rhs, rhs');
+ (* FIXME workaround based on educated guess *)
+ val prefix' = Binding.prefix_of b';
+ val is_canonical_class = is_class andalso
+ (Binding.eq_name (b, b')
+ andalso not (null prefix')
+ andalso List.last prefix' = (Class_Target.class_prefix target, false)
+ orelse same_shape);
+ in
+ not is_canonical_class ?
+ (Context.mapping_result
+ (Sign.add_abbrev Print_Mode.internal arg)
+ (ProofContext.add_abbrev Print_Mode.internal arg)
+ #-> (fn (lhs' as Const (d, _), _) =>
+ same_shape ?
+ (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
+ Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
+ end;
+
+
(* mixfix notation *)
local
@@ -222,33 +249,6 @@
end;
-(* consts *)
-
-fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
- let
- val b' = Morphism.binding phi b;
- val rhs' = Morphism.term phi rhs;
- val arg = (b', Term.close_schematic_term rhs');
- val same_shape = Term.aconv_untyped (rhs, rhs');
- (* FIXME workaround based on educated guess *)
- val prefix' = Binding.prefix_of b';
- val is_canonical_class = is_class andalso
- (Binding.eq_name (b, b')
- andalso not (null prefix')
- andalso List.last prefix' = (Class_Target.class_prefix target, false)
- orelse same_shape);
- in
- not is_canonical_class ?
- (Context.mapping_result
- (Sign.add_abbrev Print_Mode.internal arg)
- (ProofContext.add_abbrev Print_Mode.internal arg)
- #-> (fn (lhs' as Const (d, _), _) =>
- same_shape ?
- (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
- Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
- end;
-
-
(* abbrev *)
fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =