# HG changeset patch
# User haftmann
# Date 1281361225 -7200
# Node ID b1738c40c2a77807e091dfe5b76f920bdf2fd8d9
# Parent  36b20361e2a5b4b74a3b7a72c0da34a68c5d97fa# Parent  878505b05ec4915b9fd5a2468515fe6f74545b08
merged

diff -r 36b20361e2a5 -r b1738c40c2a7 src/Pure/Isar/theory_target.ML
--- 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;