# HG changeset patch
# User haftmann
# Date 1400770789 -7200
# Node ID 6a8a01e6dcdf9a8a97915dab005c6b428383dd2c
# Parent  05ed6e88089e89da88a879b08384ca95a877cc1b
tuned

diff -r 05ed6e88089e -r 6a8a01e6dcdf src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu May 22 16:59:49 2014 +0200
+++ b/src/Pure/Isar/class.ML	Thu May 22 16:59:49 2014 +0200
@@ -316,21 +316,25 @@
 
 local
 
-fun target_extension f class =
-  Local_Theory.raw_theory f
-  #> synchronize_class_syntax_target class;
+fun target_extension f class b_mx_rhs lthy =
+  let
+    val phi = morphism (Proof_Context.theory_of lthy) class;
+  in
+    lthy
+    |> Local_Theory.raw_theory (f class phi b_mx_rhs)
+    |> synchronize_class_syntax_target class
+  end;
 
-fun class_const class ((b, mx), rhs) (type_params, term_params) thy =
+fun class_const (type_params, term_params) class phi ((b, mx), rhs) thy =
   let
-    val morph = morphism thy class;
     val class_params = map fst (these_params thy [class]);
     val additional_params =
       subtract (fn (v, Free (w, _)) => v = w | _ => false) class_params term_params;
-    val context_params = map (Morphism.term morph) (type_params @ additional_params);
-    val b' = Morphism.binding morph b;
-    val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b');
+    val context_params = map (Morphism.term phi) (type_params @ additional_params);
+    val b' = Morphism.binding phi b;
+    val b_def = Morphism.binding phi (Binding.suffix_name "_dict" b');
     val c' = Sign.full_name thy b';
-    val rhs' = Morphism.term morph rhs;
+    val rhs' = Morphism.term phi rhs;
     val ty' = map Term.fastype_of context_params ---> Term.fastype_of rhs';
     val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), context_params), rhs')
       |> map_types Type.strip_sorts;
@@ -346,11 +350,10 @@
     |> Sign.add_const_constraint (c', SOME ty')
   end;
 
-fun class_abbrev class prmode ((b, mx), rhs) thy =
+fun class_abbrev prmode class phi ((b, mx), rhs) thy =
   let
-    val morph = morphism thy class;
     val unchecks = these_unchecks thy [class];
-    val b' = Morphism.binding morph b;
+    val b' = Morphism.binding phi b;
     val c' = Sign.full_name thy b';
     val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
     val ty' = Term.fastype_of rhs';
@@ -365,8 +368,8 @@
 
 in
 
-fun const class b_mx_rhs params = target_extension (class_const class b_mx_rhs params) class;
-fun abbrev class prmode b_mx_rhs = target_extension (class_abbrev class prmode b_mx_rhs) class;
+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;
 
 end;