simplified syntax for class parameters

--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 24 17:48:39 2008 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 24 17:48:40 2008 +0200
@@ -1050,9 +1050,7 @@
     ;
 
     'code\_class' (class + 'and') \\
-      ( ( '(' target \\
-        ( ( string ('where' \\
-          ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + )
+      ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
     ;
 
     'code\_instance' (( typeconstructor '::' class ) + 'and') \\
@@ -1135,10 +1133,9 @@
   serialization deletes an existing serialization.
 
   \item [@{command (HOL) "code_class"}] associates a list of classes
-  with target-specific class names; in addition, constants associated
-  with this class may be given target-specific names used for instance
-  declarations; omitting a serialization deletes an existing
-  serialization.  This applies only to \emph{Haskell}.
+  with target-specific class names; omitting a
+  serialization deletes an existing serialization.
+  This applies only to \emph{Haskell}.
 
   \item [@{command (HOL) "code_instance"}] declares a list of type
   constructor / class instance relations as ``already present'' for a

--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 24 17:48:39 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 24 17:48:40 2008 +0200
@@ -1053,9 +1053,7 @@
     ;
 
     'code\_class' (class + 'and') \\
-      ( ( '(' target \\
-        ( ( string ('where' \\
-          ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + )
+      ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
     ;
 
     'code\_instance' (( typeconstructor '::' class ) + 'and') \\
@@ -1135,10 +1133,9 @@
   serialization deletes an existing serialization.
 
   \item [\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}] associates a list of classes
-  with target-specific class names; in addition, constants associated
-  with this class may be given target-specific names used for instance
-  declarations; omitting a serialization deletes an existing
-  serialization.  This applies only to \emph{Haskell}.
+  with target-specific class names; omitting a
+  serialization deletes an existing serialization.
+  This applies only to \emph{Haskell}.
 
   \item [\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}] declares a list of type
   constructor / class instance relations as ``already present'' for a

--- a/src/HOL/Code_Setup.thy	Fri Oct 24 17:48:39 2008 +0200
+++ b/src/HOL/Code_Setup.thy	Fri Oct 24 17:48:40 2008 +0200
@@ -123,7 +123,7 @@
 text {* using built-in Haskell equality *}
 
 code_class eq
-  (Haskell "Eq" where "eq_class.eq" \<equiv> "(==)")
+  (Haskell "Eq")
 
 code_const "eq_class.eq"
   (Haskell infixl 4 "==")

--- a/src/Tools/code/code_haskell.ML	Fri Oct 24 17:48:39 2008 +0200
+++ b/src/Tools/code/code_haskell.ML	Fri Oct 24 17:48:40 2008 +0200
@@ -38,12 +38,7 @@
     val deresolve_base = NameSpace.base o deresolve;
     fun class_name class = case syntax_class class
      of NONE => deresolve class
-      | SOME (class, _) => class;
-    fun classparam_name class classparam = case syntax_class class
-     of NONE => deresolve_base classparam
-      | SOME (_, classparam_syntax) => case classparam_syntax classparam
-         of NONE => (snd o Code_Name.dest_name) classparam
-          | SOME classparam => classparam;
+      | SOME class => class;
     fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
      of [] => []
       | classbinds => Pretty.enum "," "(" ")" (
@@ -231,7 +226,7 @@
             val tyvars = Code_Name.intro_vars [v] init_syms;
             fun pr_classparam (classparam, ty) =
               semicolon [
-                (str o classparam_name name) classparam,
+                (str o deresolve_base) classparam,
                 str "::",
                 pr_typ tyvars NOBR ty
               ]
@@ -248,13 +243,34 @@
           end
       | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
           let
+            val split_abs_pure = (fn (v, _) `|-> t => SOME (v, t) | _ => NONE);
+            val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
             val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
-            fun pr_instdef ((classparam, c_inst), (thm, _)) =
-              semicolon [
-                (str o classparam_name class) classparam,
-                str "=",
-                pr_app tyvars thm false init_syms NOBR (c_inst, [])
-              ];
+            fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
+             of NONE => semicolon [
+                    (str o deresolve_base) classparam,
+                    str "=",
+                    pr_app tyvars thm false init_syms NOBR (c_inst, [])
+                  ]
+              | SOME (k, pr) =>
+                  let
+                    val (c_inst_name, (_, tys)) = c_inst;
+                    val const = if (is_some o syntax_const) c_inst_name
+                      then NONE else (SOME o NameSpace.base o deresolve) c_inst_name;
+                    val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
+                    val (vs, rhs) = unfold_abs_pure proto_rhs;
+                    val vars = init_syms
+                      |> Code_Name.intro_vars (the_list const)
+                      |> Code_Name.intro_vars vs;
+                    val lhs = IConst (classparam, ([], tys)) `$$ map IVar vs;
+                      (*dictionaries are not relevant at this late stage*)
+                  in
+                    semicolon [
+                      pr_term tyvars thm false vars NOBR lhs,
+                      str "=",
+                      pr_term tyvars thm false vars NOBR rhs
+                    ]
+                  end;
           in
             Pretty.block_enclose (
               Pretty.block [