# HG changeset patch
# User bulwahn
# Date 1315396296 -7200
# Node ID fddb09e6f84dd5ebd64d094dbb8592f2a51e81be
# Parent  26b19918e670c1b1ac1c462571912ca23b553b16
removing previous crude approximation to add type annotations to disambiguate types

diff -r 26b19918e670 -r fddb09e6f84d src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Wed Sep 07 13:51:35 2011 +0200
+++ b/src/Tools/Code/code_haskell.ML	Wed Sep 07 13:51:36 2011 +0200
@@ -25,7 +25,7 @@
 (** Haskell serializer **)
 
 fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax
-    reserved deresolve contr_classparam_typs deriving_show =
+    reserved deresolve deriving_show =
   let
     fun class_name class = case class_syntax class
      of NONE => deresolve class
@@ -298,7 +298,6 @@
       labelled_name module_alias module_prefix (Name.make_context reserved) program;
 
     (* print statements *)
-    val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
     fun deriving_show tyco =
       let
         fun deriv _ "fun" = false
@@ -314,7 +313,7 @@
       in deriv [] tyco end;
     fun print_stmt deresolve = print_haskell_stmt labelled_name
       class_syntax tyco_syntax const_syntax (make_vars reserved)
-      deresolve contr_classparam_typs
+      deresolve
       (if string_classes then deriving_show else K false);
 
     (* print modules *)
diff -r 26b19918e670 -r fddb09e6f84d src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:35 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:36 2011 +0200
@@ -88,7 +88,6 @@
   val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
   val is_cons: program -> string -> bool
   val is_case: stmt -> bool
-  val contr_classparam_typs: program -> string -> itype option list
   val labelled_name: theory -> program -> string -> string
   val group_stmts: theory -> program
     -> ((string * stmt) list * (string * stmt) list
@@ -481,28 +480,6 @@
   (fn (_, (Classinst ((class, _), (_, (param_insts, _))), _)) =>
     Option.map (fn ((const, _), _) => (class, const))
       (find_first (fn ((_, (inst_const, _)), _) => inst_const = name) param_insts) | _ => NONE)
-
-fun contr_classparam_typs program name = 
-  let
-    fun contr_classparam_typs' (class, name) =
-      let
-        val Class (_, (_, (_, params))) = Graph.get_node program class;
-        val SOME ty = AList.lookup (op =) params name;
-        val (tys, res_ty) = unfold_fun ty;
-        fun no_tyvar (_ `%% tys) = forall no_tyvar tys
-          | no_tyvar (ITyVar _) = false;
-      in if no_tyvar res_ty
-        then map (fn ty => if no_tyvar ty then NONE else SOME ty) tys
-        else []
-      end
- in 
-   case Graph.get_node program name
-   of Classparam (_, class) => contr_classparam_typs' (class, name)
-    | Fun (c, _) => (case lookup_classparam_instance program name
-      of NONE => []
-       | SOME (class, name) => the_default [] (try contr_classparam_typs' (class, name)))
-    | _ => []
-  end;
   
 fun labelled_name thy program name =
   let val ctxt = Proof_Context.init_global thy in