--- a/src/Pure/Isar/theory_target.ML Mon Aug 09 15:40:06 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML Mon Aug 09 15:40:25 2010 +0200
@@ -158,7 +158,7 @@
in (result'', result) end;
-fun theory_notes kind global_facts local_facts lthy =
+fun theory_notes kind global_facts lthy =
let
val thy = ProofContext.theory_of lthy;
val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
@@ -190,11 +190,38 @@
in
lthy
|> (if is_locale then locale_notes target kind global_facts local_facts
- else theory_notes kind global_facts local_facts)
+ else theory_notes kind global_facts)
|> ProofContext.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts)
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,34 +249,14 @@
end;
-(* consts *)
+(* abbrev *)
-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) (*guesses class constants*)
- orelse same_shape (*guesses class abbrevs*));
- 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;
+fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory
+ (Sign.add_abbrev (#1 prmode) (b, t) #-> (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
-
-(* abbrev *)
+fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result
+ (Sign.add_abbrev Print_Mode.internal (b, t)) #-> (fn (lhs, _) =>
+ syntax_declaration ta false (locale_const ta prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))));
fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
let
@@ -268,17 +275,9 @@
singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
in
lthy |>
- (if is_locale then
- Local_Theory.theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs))
- #-> (fn (lhs, _) =>
- let val lhs' = Term.list_comb (Logic.unvarify_global lhs, xs) in
- syntax_declaration ta false (locale_const ta prmode ((b, mx2), lhs')) #>
- is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t'))
- end)
- else
- Local_Theory.theory
- (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) =>
- Sign.notation true prmode [(lhs, mx3)])))
+ (if is_locale then locale_abbrev ta prmode ((b, mx2), global_rhs) xs #>
+ is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t'))
+ else theory_abbrev prmode ((b, mx3), global_rhs))
|> ProofContext.add_abbrev Print_Mode.internal (b, t) |> snd
|> Local_Defs.fixed_abbrev ((b, NoSyn), t)
end;