src/Pure/Isar/code.ML

--- a/src/Pure/Isar/code.ML	Mon Oct 05 08:36:33 2009 +0200
+++ b/src/Pure/Isar/code.ML	Mon Oct 05 15:04:45 2009 +0200
@@ -13,7 +13,6 @@
   val read_const: theory -> string -> string
   val string_of_const: theory -> string -> string
   val args_number: theory -> string -> int
-  val typscheme: theory -> string * typ -> (string * sort) list * typ
 
   (*constructor sets*)
   val constrset_of_consts: theory -> (string * typ) list
@@ -28,8 +27,7 @@
     -> (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
+  val typscheme_eqns: theory -> string -> thm list -> (string * sort) list * typ
 
   (*executable code*)
   val add_datatype: (string * typ) list -> theory -> theory
@@ -114,19 +112,6 @@
 
 fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
 
-fun typscheme thy (c, ty) =
-  let
-    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 **)
@@ -522,18 +507,22 @@
     val (c, ty) = head_eqn thm;
     val c' = AxClass.unoverload_const thy (c, ty);
   in (c', ty) end;
-
-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 typscheme thy (c, ty) =
+  (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
+fun typscheme_eqn thy = typscheme thy o apsnd Logic.unvarifyT o const_typ_eqn thy;
+fun typscheme_eqns thy c [] = 
+      let
+        val raw_ty = Sign.the_const_type thy c;
+        val tvars = Term.add_tvar_namesT raw_ty [];
+        val tvars' = case AxClass.class_of_param thy c
+         of SOME class => [TFree (Name.aT, [class])]
+          | NONE => Name.invent_list [] Name.aT (length tvars)
+              |> map (fn v => TFree (v, []));
+        val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
+      in typscheme thy (c, ty) end
+  | typscheme_eqns thy c (thms as thm :: _) = typscheme_eqn thy thm;
 
 fun assert_eqns_const thy c eqns =
   let
@@ -549,7 +538,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 "'X" sorts
+    val vts = Name.names Name.context Name.aT sorts
       |> map (fn (v, sort) => TVar ((v, 0), sort));
   in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end;