tuned abbreviations in class context

--- a/src/Pure/Isar/class.ML	Mon Oct 22 16:54:50 2007 +0200
+++ b/src/Pure/Isar/class.ML	Mon Oct 22 16:54:52 2007 +0200
@@ -315,9 +315,9 @@
     (*partial morphism of canonical interpretation*)
   intro: thm,
   defs: thm list,
-  operations: (string * (((term * typ) * (typ * int)) * term)) list
-    (*constant name ~> ((locale term & typ,
-        (constant constraint, instantiaton index of class typ)), locale term for uncheck)*)
+  operations: (string * ((term * (typ * int)) * (term * typ))) list
+    (*constant name ~> ((locale term,
+        (constant constraint, instantiaton index of class typ)), locale term & typ for uncheck)*)
 };
 
 fun rep_class_data (ClassData d) = d;
@@ -439,7 +439,7 @@
       (SOME o the o Symtab.lookup insttab o fst o fst)
         (Locale.parameters_of_expr thy (Locale.Locale class));
     val operations = map (fn (v_ty as (_, ty'), (c, ty)) =>
-      (c, (((Free v_ty, ty'), (Logic.varifyT ty, 0)), Free v_ty))) cs;
+      (c, ((Free v_ty, (Logic.varifyT ty, 0)), (Free v_ty, ty')))) cs;
     val cs = (map o pairself) fst cs;
     val add_class = Graph.new_node (class,
         mk_class_data ((cs, base_sort, inst, phi, intro), ([], operations)))
@@ -448,18 +448,20 @@
     ClassData.map add_class thy
   end;
 
-fun register_operation class ((c, (dict, dict_rev)), some_def) thy =
+fun register_operation class ((c, (t, t_rev)), some_def) thy =
   let
     val ty = Sign.the_const_constraint thy c;
     val typargs = Sign.const_typargs thy (c, ty);
     val typidx = find_index (fn TVar ((v, _), _) => Name.aT = v | _ => false) typargs;
-    val ty' = Term.fastype_of dict;
+    val t_rev' = (map_types o map_atyps)
+      (fn ty as TFree (v, _) => if Name.aT = v then TFree (v, []) else ty | ty => ty) t_rev;
+    val ty' = Term.fastype_of t_rev';
   in
     thy
     |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
       (fn (defs, operations) =>
         (fold cons (the_list some_def) defs,
-          (c, (((dict, ty'), (ty, typidx)), dict_rev)) :: operations))
+          (c, ((t, (ty, typidx)), (t_rev', ty'))) :: operations))
   end;
 
 
@@ -583,17 +585,13 @@
 
     (* check phase *)
     val typargs = Consts.typargs (ProofContext.consts_of ctxt);
-    fun check_const (c, ty) (((t, _), (_, idx)), _) =
+    fun check_const (c, ty) ((t, (_, idx)), _) =
       ((nth (typargs (c, ty)) idx), t);
     fun local_operation (c_ty as (c, _)) = AList.lookup (op =) operations c
       |> Option.map (check_const c_ty);
 
     (* uncheck phase *)
-    val proto_rews = map (fn (c, (((t, ty), _), _)) => (t, Const (c, ty))) operations;
-    fun rew_app f (t1 $ t2) = rew_app f t1 $ f t2
-      | rew_app f t = t;
-    val rews = (map o apfst o rew_app)
-      (Pattern.rewrite_term thy proto_rews []) proto_rews;
+    val rews = map (fn (c, (_, (t, ty))) => (t, Const (c, ty))) operations;
   in
     ctxt
     |> fold (ProofContext.add_const_constraint o local_constraint) operations
@@ -832,23 +830,6 @@
 
 (* abbreviation in class target *)
 
-fun expand_aux_abbrev thy class t =
-  let
-    val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy [class]);
-    val (head, ts) = strip_comb t;
-    val tys = (fst o chop (length ts) o fst o strip_type o Term.fastype_of) head;
-    val head' = head
-      |> Pattern.eta_long tys
-      |> Consts.certify (Sign.pp thy) (Sign.tsig_of thy) true (Sign.consts_of thy);
-    val ts' = ts
-      |> map (Pattern.rewrite_term thy rews []);
-  in Term.betapplys (head', ts') end;
-
-fun fold_aux_defs thy class =
-  let
-    val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy [class])
-  in Pattern.rewrite_term thy rews [] end;
-
 fun add_syntactic_const class prmode pos ((c, mx), rhs) thy =
   let
     val prfx = class_prefix class;
@@ -856,9 +837,10 @@
     val phi = morphism thy class;
 
     val c' = Sign.full_name thy' c;
-    val dict' = (expand_aux_abbrev thy' class o Morphism.term phi) rhs;
-    val dict'' = map_types Logic.unvarifyT dict';
-    val ty' = Term.fastype_of dict'';
+    val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy' [class])
+    val rhs' = (Pattern.rewrite_term thy rews [] o Morphism.term phi) rhs;
+    val rhs'' = map_types Logic.unvarifyT rhs';
+    val ty' = Term.fastype_of rhs'';
 
     val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
     val ty'' = (Type.strip_sorts o Logic.unvarifyT) (Sign.the_const_constraint thy' c'');
@@ -866,10 +848,10 @@
     thy'
     |> Sign.add_const_constraint (c'', SOME ty'') (*FIXME*)
     |> Sign.hide_consts_i false [c''] (*FIXME*)
-    |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts dict') |> snd
+    |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs') |> snd
     |> Sign.add_const_constraint (c', SOME ty')
     |> Sign.notation true prmode [(Const (c', ty'), mx)]
-    |> register_operation class ((c', (dict', dict'')), NONE)
+    |> register_operation class ((c', (rhs, rhs'')), NONE)
     |> Sign.restore_naming thy
   end;
 

--- a/src/Pure/Isar/theory_target.ML	Mon Oct 22 16:54:50 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML	Mon Oct 22 16:54:52 2007 +0200
@@ -215,6 +215,7 @@
     val u = fold_rev lambda xs t';
     val global_rhs =
       singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
+    val class_t = Morphism.term (LocalTheory.target_morphism lthy) t;
   in
     lthy |>
      (if is_locale then
@@ -223,7 +224,7 @@
           let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
             term_syntax ta (locale_const prmode pos ((c, mx2), lhs')) #>
             is_class ?
-              class_target ta (Class.add_syntactic_const target prmode pos ((c, mx1), lhs'))
+              class_target ta (Class.add_syntactic_const target prmode pos ((c, mx1), class_t))
           end)
       else
         LocalTheory.theory