variables in type schemes must be renamed simultaneously with variables in equations

--- a/src/Pure/Isar/code.ML	Sun Oct 04 12:59:22 2009 +0200
+++ b/src/Pure/Isar/code.ML	Mon Oct 05 08:36:33 2009 +0200
@@ -28,6 +28,8 @@
     -> (thm * bool) list -> (thm * bool) list
   val const_typ_eqn: theory -> thm -> string * typ
   val typscheme_eqn: theory -> thm -> (string * sort) list * typ
+  val typscheme_rhss_eqns: theory -> string -> thm list
+    -> ((string * sort) list * typ) * (string * typ list) list
 
   (*executable code*)
   val add_datatype: (string * typ) list -> theory -> theory
@@ -117,6 +119,15 @@
     val ty' = Logic.unvarifyT ty;
   in (map dest_TFree (Sign.const_typargs thy (c, ty')), Type.strip_sorts ty') end;
 
+fun default_typscheme thy c =
+  let
+    val ty = (snd o dest_Const o Term_Subst.zero_var_indexes o curry Const c
+      o Type.strip_sorts o Sign.the_const_type thy) c;
+  in case AxClass.class_of_param thy c
+   of SOME class => ([(Name.aT, [class])], ty)
+    | NONE => typscheme thy (c, ty)
+  end;
+
 
 (** data store **)
 
@@ -515,6 +526,15 @@
 fun typscheme_eqn thy = typscheme thy o const_typ_eqn thy;
 fun const_eqn thy = fst o const_typ_eqn thy;
 
+fun consts_of thy thms = [] |> (fold o fold o fold_aterms)
+  (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
+    (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of) thms);
+
+fun typscheme_rhss_eqns thy c [] =
+      (default_typscheme thy c, [])
+  | typscheme_rhss_eqns thy c (thms as thm :: _) =
+      (typscheme_eqn thy thm, consts_of thy thms);
+
 fun assert_eqns_const thy c eqns =
   let
     fun cert (eqn as (thm, _)) = if c = const_eqn thy thm
@@ -529,7 +549,7 @@
     fun inter_sorts vs =
       fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
     val sorts = map_transpose inter_sorts vss;
-    val vts = Name.names Name.context Name.aT sorts
+    val vts = Name.names Name.context "'X" sorts
       |> map (fn (v, sort) => TVar ((v, 0), sort));
   in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end;
 

--- a/src/Tools/Code/code_preproc.ML	Sun Oct 04 12:59:22 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML	Mon Oct 05 08:36:33 2009 +0200
@@ -227,27 +227,6 @@
   map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
     o maps (#params o AxClass.get_info thy);
 
-fun consts_of thy eqns = [] |> (fold o fold o fold_aterms)
-  (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
-    (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
-
-fun default_typscheme_of thy c =
-  let
-    val ty = (snd o dest_Const o Term_Subst.zero_var_indexes o curry Const c
-      o Type.strip_sorts o Sign.the_const_type thy) c;
-  in case AxClass.class_of_param thy c
-   of SOME class => ([(Name.aT, [class])], ty)
-    | NONE => Code.typscheme thy (c, ty)
-  end;
-
-fun tyscm_rhss_of thy c eqns =
-  let
-    val tyscm = case eqns
-     of [] => default_typscheme_of thy c
-      | ((thm, _) :: _) => Code.typscheme_eqn thy thm;
-    val rhss = consts_of thy eqns;
-  in (tyscm, rhss) end;
-
 
 (* data structures *)
 
@@ -287,7 +266,7 @@
     | NONE => let
         val eqns = Code.these_eqns thy c
           |> preprocess thy c;
-        val ((lhs, _), rhss) = tyscm_rhss_of thy c eqns;
+        val ((lhs, _), rhss) = Code.typscheme_rhss_eqns thy c (map fst eqns);
       in ((lhs, rhss), eqns) end;
 
 fun obtain_instance thy arities (inst as (class, tyco)) =
@@ -434,7 +413,7 @@
       Vartab.update ((v, 0), sort)) lhs;
     val eqns = proto_eqns
       |> (map o apfst) (inst_thm thy inst_tab);
-    val (tyscm, rhss') = tyscm_rhss_of thy c eqns;
+    val (tyscm, rhss') = Code.typscheme_rhss_eqns thy c (map fst eqns);
     val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
   in (map (pair c) rhss' @ rhss, eqngr') end;
 

--- a/src/Tools/Code/code_thingol.ML	Sun Oct 04 12:59:22 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Oct 05 08:36:33 2009 +0200
@@ -554,16 +554,21 @@
     fun stmt_classparam class =
       ensure_class thy algbr funcgr class
       #>> (fn class => Classparam (c, class));
-    fun stmt_fun ((vs, ty), eqns) =
-      fold_map (translate_tyvar_sort thy algbr funcgr) vs
-      ##>> translate_typ thy algbr funcgr ty
-      ##>> fold_map (translate_eqn thy algbr funcgr) (burrow_fst (clean_thms thy) eqns)
-      #>> (fn info => Fun (c, info));
+    fun stmt_fun raw_eqns =
+      let
+        val eqns = burrow_fst (clean_thms thy) raw_eqns;
+        val ((vs, ty), _) = Code.typscheme_rhss_eqns thy c (map fst eqns);
+      in
+        fold_map (translate_tyvar_sort thy algbr funcgr) vs
+        ##>> translate_typ thy algbr funcgr ty
+        ##>> fold_map (translate_eqn thy algbr funcgr) eqns
+        #>> (fn info => Fun (c, info))
+      end;
     val stmt_const = case Code.get_datatype_of_constr thy c
      of SOME tyco => stmt_datatypecons tyco
       | NONE => (case AxClass.class_of_param thy c
          of SOME class => stmt_classparam class
-          | NONE => stmt_fun (Code_Preproc.typ funcgr c, Code_Preproc.eqns funcgr c))
+          | NONE => stmt_fun (Code_Preproc.eqns funcgr c))
   in ensure_stmt lookup_const (declare_const thy) stmt_const c end
 and ensure_class thy (algbr as (_, algebra)) funcgr class =
   let