# HG changeset patch
# User haftmann
# Date 1400773981 -7200
# Node ID dfac6ef0ca2809d696856f247b4423c32dbc6b71
# Parent  c97b8250c033c2cd3490b6b0ec8dc88a82b9b495
moved const declaration further down in bootstrap hierarchy: keep Named_Target free of low-level stuff

diff -r c97b8250c033 -r dfac6ef0ca28 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu May 22 17:52:59 2014 +0200
+++ b/src/Pure/Isar/class.ML	Thu May 22 17:53:01 2014 +0200
@@ -18,7 +18,7 @@
   val init: class -> theory -> Proof.context
   val begin: class list -> sort -> Proof.context -> Proof.context
   val const: class -> (binding * mixfix) * term -> term list * term list -> local_theory -> local_theory
-  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
+  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> term -> local_theory -> local_theory
   val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
   val class_prefix: string -> string
   val register: class -> class list -> ((string * typ) * (string * typ)) list
@@ -325,6 +325,26 @@
     |> synchronize_class_syntax_target class
   end;
 
+fun const_declaration class prmode (b, rhs) =
+  Generic_Target.locale_declaration class true (fn phi =>
+    let
+      val b' = Morphism.binding phi b;
+      val rhs' = Morphism.term phi 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 = 
+        Binding.eq_name (b, b')
+          andalso not (null prefix')
+          andalso List.last prefix' = (class_prefix class, false)
+        orelse same_shape;
+    in
+      not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', NoSyn), rhs')
+    end) #>
+  Generic_Target.const_declaration
+    (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, NoSyn), rhs);
+
 fun class_const (type_params, term_params) class phi ((b, mx), rhs) thy =
   let
     val class_params = map fst (these_params thy [class]);
@@ -368,8 +388,13 @@
 
 in
 
-fun const class b_mx_rhs params = target_extension (class_const params) class b_mx_rhs;
-fun abbrev class prmode b_mx_rhs = target_extension (class_abbrev prmode) class b_mx_rhs;
+fun const class ((b, mx), lhs) params =
+  const_declaration class Syntax.mode_default (b, lhs)
+  #> target_extension (class_const params) class ((b, mx), lhs);
+
+fun abbrev class prmode ((b, mx), lhs) t' =
+  const_declaration class prmode (b, lhs)
+  #> target_extension (class_abbrev prmode) class ((b, mx), t');
 
 end;
 
diff -r c97b8250c033 -r dfac6ef0ca28 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu May 22 17:52:59 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu May 22 17:53:01 2014 +0200
@@ -31,6 +31,8 @@
     Context.generic -> Context.generic
   val const_declaration: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
+  val locale_const_declaration: string -> Syntax.mode -> (binding * mixfix) * term ->
+    local_theory -> local_theory
   val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
   val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
@@ -280,6 +282,16 @@
       val same_shape = Term.aconv_untyped (rhs, rhs');
     in generic_const same_shape prmode ((b', mx), rhs') end);
 
+fun locale_const_declaration locale prmode ((b, mx), rhs) =
+  locale_declaration locale true (fn phi =>
+    let
+      val b' = Morphism.binding phi b;
+      val rhs' = Morphism.term phi rhs;
+      val same_shape = Term.aconv_untyped (rhs, rhs');
+    in generic_const same_shape prmode ((b', mx), rhs') end)
+  #> const_declaration
+    (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
+
 
 (* registrations and dependencies *)
 
diff -r c97b8250c033 -r dfac6ef0ca28 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Thu May 22 17:52:59 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu May 22 17:53:01 2014 +0200
@@ -48,52 +48,16 @@
   Option.map #target (peek lthy) = SOME "" andalso Local_Theory.level lthy = 1;
 
 
-(* consts *)
-
-fun locale_const locale prmode ((b, mx), rhs) =
-  Generic_Target.locale_declaration locale true (fn phi =>
-    let
-      val b' = Morphism.binding phi b;
-      val rhs' = Morphism.term phi rhs;
-      val same_shape = Term.aconv_untyped (rhs, rhs');
-    in
-      Generic_Target.generic_const same_shape prmode ((b', mx), rhs')
-    end) #>
-  Generic_Target.const_declaration
-    (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
-
-fun class_const class prmode (b, rhs) =
-  Generic_Target.locale_declaration class true (fn phi =>
-    let
-      val b' = Morphism.binding phi b;
-      val rhs' = Morphism.term phi 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 = 
-        Binding.eq_name (b, b')
-          andalso not (null prefix')
-          andalso List.last prefix' = (Class.class_prefix class, false)
-        orelse same_shape;
-    in
-      not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', NoSyn), rhs')
-    end) #>
-  Generic_Target.const_declaration
-    (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, NoSyn), rhs);
-
-
 (* define *)
 
 fun locale_foundation target (((b, U), mx), (b_def, rhs)) params =
   Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params
-  #-> (fn (lhs, def) => locale_const target Syntax.mode_default ((b, mx), lhs)
+  #-> (fn (lhs, def) => Generic_Target.locale_const_declaration target Syntax.mode_default ((b, mx), lhs)
     #> pair (lhs, def));
 
 fun class_foundation target (((b, U), mx), (b_def, rhs)) params =
   Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params
-  #-> (fn (lhs, def) => class_const target Syntax.mode_default (b, lhs)
-    #> Class.const target ((b, mx), lhs) params
+  #-> (fn (lhs, def) => Class.const target ((b, mx), lhs) params
     #> pair (lhs, def));
 
 fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
@@ -114,13 +78,11 @@
 fun locale_abbrev target prmode (b, mx) (t, _) xs =
   Generic_Target.background_abbrev (b, t)
   #-> (fn (lhs, _) =>
-        locale_const target prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
+        Generic_Target.locale_const_declaration target prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
 
 fun class_abbrev target prmode (b, mx) (t, t') xs =
   Generic_Target.background_abbrev (b, t)
-  #-> (fn (lhs, _) =>
-        class_const target prmode (b, Term.list_comb (Logic.unvarify_global lhs, xs)))
-  #> Class.abbrev target prmode ((b, mx), t');
+  #-> (fn (lhs, _) => Class.abbrev target prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)) t');
 
 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) =
   if is_class then class_abbrev target