# HG changeset patch
# User haftmann
# Date 1191519712 -7200
# Node ID 1d1bddf873531151c979ef186bd991ccd92d2051
# Parent  cacc5744be755ff9a54e7b0162cef5517e1de571
put declarations first

diff -r cacc5744be75 -r 1d1bddf87353 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Oct 04 19:41:51 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML	Thu Oct 04 19:41:52 2007 +0200
@@ -51,6 +51,36 @@
   end;
 
 
+(* target declarations *)
+
+fun target_morphism loc lthy =
+  ProofContext.export_morphism lthy (LocalTheory.target_of lthy) $>
+  Morphism.thm_morphism Goal.norm_result;
+
+fun target_decl add loc d lthy =
+  let
+    val d' = Morphism.transform (target_morphism loc lthy) d;
+    val d0 = Morphism.form d';
+  in
+    if loc = "" then
+      lthy
+      |> LocalTheory.theory (Context.theory_map d0)
+      |> LocalTheory.target (Context.proof_map d0)
+    else
+      lthy
+      |> LocalTheory.target (add loc d')
+  end;
+
+val type_syntax = target_decl Locale.add_type_syntax;
+val term_syntax = target_decl Locale.add_term_syntax;
+val declaration = target_decl Locale.add_declaration;
+
+fun target_naming loc lthy =
+  (if loc = "" then Sign.naming_of (ProofContext.theory_of lthy)
+   else ProofContext.naming_of (LocalTheory.target_of lthy))
+  |> NameSpace.qualified_names;
+
+
 (* consts *)
 
 fun target_abbrev prmode ((c, mx), rhs) phi =
@@ -151,15 +181,14 @@
     val u = fold_rev Term.lambda xs t;
     val U = Term.fastype_of u;
     val u' = singleton (Variable.export_terms (Variable.declare_term u target) thy_ctxt) u;
-
-    val ((lhs as Const (full_c, _), rhs), lthy1) = lthy |> LocalTheory.theory_result
-      (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u'));
     val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx;
   in
-    lthy1
-    |> LocalTheory.theory (Sign.add_notation prmode [(lhs, mx1)])
-    |> is_loc ? internal_abbrev prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs))
-    |> local_abbrev (c, rhs)
+    lthy
+    |> LocalTheory.theory_result
+        (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u'))
+    |-> (fn (lhs as Const (full_c, _), rhs) => LocalTheory.theory (Sign.add_notation prmode [(lhs, mx1)])
+    #> is_loc ? internal_abbrev prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs))
+    #> local_abbrev (c, rhs))
   end;
 
 
@@ -337,36 +366,6 @@
   end;
 
 
-(* target declarations *)
-
-fun target_decl add loc d lthy =
-  let
-    val d' = Morphism.transform (LocalTheory.target_morphism lthy) d;
-    val d0 = Morphism.form d';
-  in
-    if loc = "" then
-      lthy
-      |> LocalTheory.theory (Context.theory_map d0)
-      |> LocalTheory.target (Context.proof_map d0)
-    else
-      lthy
-      |> LocalTheory.target (add loc d')
-  end;
-
-val type_syntax = target_decl Locale.add_type_syntax;
-val term_syntax = target_decl Locale.add_term_syntax;
-val declaration = target_decl Locale.add_declaration;
-
-fun target_morphism loc lthy =
-  ProofContext.export_morphism lthy (LocalTheory.target_of lthy) $>
-  Morphism.thm_morphism Goal.norm_result;
-
-fun target_naming loc lthy =
-  (if loc = "" then Sign.naming_of (ProofContext.theory_of lthy)
-   else ProofContext.naming_of (LocalTheory.target_of lthy))
-  |> NameSpace.qualified_names;
-
-
 (* init and exit *)
 
 fun begin loc ctxt =