# HG changeset patch
# User haftmann
# Date 1402263047 -7200
# Node ID de00494fa8b30e84d038ce7d0359c9ee5f846ea1
# Parent  63c7b29d29accf0885240ccb210156131007f512
less ad-hoc verision of educated guess: guess identity of declaration morphism wrt. canonical morphism rather than observing particular effects of declaration morphisms only;
n.b. this fullfills promise given in 63c7b29d29ac

diff -r 63c7b29d29ac -r de00494fa8b3 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Jun 07 21:49:17 2014 +0200
+++ b/src/Pure/Isar/class.ML	Sun Jun 08 23:30:47 2014 +0200
@@ -323,22 +323,26 @@
 
 local
 
-fun class_const class prmode ((b, mx), rhs) =
+fun guess_morphism_identity (b, rhs) phi1 phi2 =
+  let
+    (*FIXME proper concept to identify morphism instead of educated guess*)
+    val name_of_binding = Name_Space.full_name Name_Space.default_naming;
+    val n1 = (name_of_binding o Morphism.binding phi1) b;
+    val n2 = (name_of_binding o Morphism.binding phi2) b;
+    val rhs1 = Morphism.term phi1 rhs;
+    val rhs2 = Morphism.term phi2 rhs;
+  in n1 = n2 andalso Term.aconv_untyped (rhs1, rhs2) end;
+
+fun class_const class phi0 prmode ((b, mx), 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;
+      val is_plain = guess_morphism_identity (b, rhs) Morphism.identity phi;
+      val is_canonical = guess_morphism_identity (b, rhs) phi0 phi;
     in
-      not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs')
+      not (is_plain orelse is_canonical) ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs')
     end);
 
 fun dangling_params_for lthy class (type_params, term_params) =
@@ -398,7 +402,7 @@
     val dangling_params = map (Morphism.term phi) (uncurry append (dangling_params_for lthy class params));
   in
     lthy
-    |> class_const class Syntax.mode_default ((b, mx), lhs)
+    |> class_const class phi Syntax.mode_default ((b, mx), lhs)
     |> Local_Theory.raw_theory (canonical_const class phi dangling_params
          ((Morphism.binding phi b, if null dangling_params then mx else NoSyn), Morphism.term phi lhs))
     |> Generic_Target.const (fn (this, other) => other <> 0 andalso this <> other)
@@ -412,7 +416,7 @@
     val dangling_term_params = map (Morphism.term phi) (snd (dangling_params_for lthy class params));
   in
     lthy
-    |> class_const class prmode ((b, mx), lhs)
+    |> class_const class phi prmode ((b, mx), lhs)
     |> Local_Theory.raw_theory (canonical_abbrev class phi prmode dangling_term_params
          ((Morphism.binding phi b, if null dangling_term_params then mx else NoSyn), rhs'))
     |> Generic_Target.const (fn (this, other) => other <> 0 andalso this <> other)