# HG changeset patch
# User haftmann
# Date 1401604415 -7200
# Node ID 9d6f733ef45647353c9a0221b2738f653a97944f
# Parent  728fa98b7fdf6dee1e0e9543fa0a51acd3fd45e4
tuned

diff -r 728fa98b7fdf -r 9d6f733ef456 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat May 31 23:00:13 2014 +0200
+++ b/src/Pure/Isar/class.ML	Sun Jun 01 08:33:35 2014 +0200
@@ -352,22 +352,19 @@
 
 fun canonical_const class phi dangling_params ((b, mx), rhs) thy =
   let
-    val dangling_params' = map (Morphism.term phi) dangling_params;
-    val b' = Morphism.binding phi b;
-    val b_def = Binding.suffix_name "_dict" b';
-    val rhs' = Morphism.term phi rhs;
-    val c' = Sign.full_name thy b';
-    val ty' = map Term.fastype_of dangling_params' ---> Term.fastype_of rhs';
-    val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), dangling_params'), rhs')
+    val b_def = Binding.suffix_name "_dict" b;
+    val c = Sign.full_name thy b;
+    val ty = map Term.fastype_of dangling_params ---> Term.fastype_of rhs;
+    val def_eq = Logic.mk_equals (list_comb (Const (c, ty), dangling_params), rhs)
       |> map_types Type.strip_sorts;
   in
     thy
-    |> Sign.declare_const_global ((b', Type.strip_sorts ty'), mx)
+    |> Sign.declare_const_global ((b, Type.strip_sorts ty), mx)
     |> snd
     |> global_def (b_def, def_eq)
     |-> (fn def_thm =>
-      null dangling_params' ? register_operation class (c', (rhs', SOME (Thm.symmetric def_thm))))
-    |> Sign.add_const_constraint (c', SOME ty')
+      null dangling_params ? register_operation class (c, (rhs, SOME (Thm.symmetric def_thm))))
+    |> Sign.add_const_constraint (c, SOME ty)
   end;
 
 fun canonical_abbrev class phi prmode ((b, mx), rhs) thy =
@@ -390,12 +387,13 @@
 
 fun const class ((b, mx), lhs) params lthy =
   let
-    val dangling_params = dangling_params_for lthy class params;
     val phi = morphism (Proof_Context.theory_of lthy) class;
+    val dangling_params = map (Morphism.term phi) (dangling_params_for lthy class params);
   in
     lthy
     |> class_const class Syntax.mode_default (b, lhs)
-    |> Local_Theory.raw_theory (canonical_const class phi dangling_params ((b, mx), lhs))
+    |> Local_Theory.raw_theory
+        (canonical_const class phi dangling_params ((Morphism.binding phi b, mx), Morphism.term phi lhs))
     |> Generic_Target.const (fn (this, other) => other <> 0 andalso this <> other) Syntax.mode_default ((b, NoSyn), lhs)
     |> synchronize_class_syntax_target class
   end;