# HG changeset patch
# User haftmann
# Date 1401521712 -7200
# Node ID 3e083fb1218aa9f70163316c886452b62842bcd3
# Parent  ad09e59f50a9dd2c6915b3b27d0c3645eb21e4d7
postpone const declarations for nested context after canonical const declarations: keep const declarations stemming from interpretation together

diff -r ad09e59f50a9 -r 3e083fb1218a src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat May 31 09:35:10 2014 +0200
+++ b/src/Pure/Isar/class.ML	Sat May 31 09:35:12 2014 +0200
@@ -332,8 +332,7 @@
         orelse same_shape;
     in
       not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', NoSyn), rhs')
-    end) #>
-  Generic_Target.const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, NoSyn), rhs);
+    end);
 
 fun dangling_params_for lthy class (type_params, term_params) =
   let
@@ -397,6 +396,7 @@
     lthy
     |> class_const class Syntax.mode_default (b, lhs)
     |> Local_Theory.raw_theory (canonical_const class phi dangling_params ((b, mx), lhs))
+    |> Generic_Target.const (fn (this, other) => other <> 0 andalso this <> other) Syntax.mode_default ((b, NoSyn), lhs)
     |> synchronize_class_syntax_target class
   end;
 
@@ -407,6 +407,7 @@
     lthy
     |> class_const class prmode (b, lhs)
     |> Local_Theory.raw_theory (canonical_abbrev class phi prmode ((b, mx), rhs'))
+    |> Generic_Target.const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, NoSyn), lhs)
     |> synchronize_class_syntax_target class
   end;