# HG changeset patch
# User haftmann
# Date 1281361126 -7200
# Node ID 878505b05ec4915b9fd5a2468515fe6f74545b08
# Parent  e0ad785031860767f19971b5808e38ea5d278481
dropped idle local_facts argument; factored out theory_abbrev and locale_abbrev

diff -r e0ad78503186 -r 878505b05ec4 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Aug 09 15:20:50 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Mon Aug 09 15:38:46 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,7 +190,7 @@
   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;
 
@@ -251,6 +251,13 @@
 
 (* abbrev *)
 
+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)]));
+
+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
     val thy_ctxt = ProofContext.init_global (ProofContext.theory_of lthy);
@@ -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;