# HG changeset patch
# User haftmann
# Date 1290883288 -3600
# Node ID 1ef64dcb24b750ee8e5fb457d0eacf301ac4195a
# Parent  86c43003742d20a507e80bf641167a5081640f91
corrected: use canonical variables of type scheme uniformly

diff -r 86c43003742d -r 1ef64dcb24b7 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Nov 27 19:41:27 2010 +0100
+++ b/src/Pure/Isar/code.ML	Sat Nov 27 19:41:28 2010 +0100
@@ -742,16 +742,16 @@
 
 fun empty_cert thy c = 
   let
-    val raw_ty = const_typ 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 =>  (case get_type_of_constr_or_abstr thy c
-         of SOME (tyco, _) => map TFree ((fst o the)
-              (AList.lookup (op =) ((snd o fst o get_type thy) tyco) c))
-          | NONE => Name.invent_list [] Name.aT (length tvars)
-              |> map (fn v => TFree (v, [])));
-    val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
+    val raw_ty = Logic.unvarifyT_global (const_typ thy c);
+    val (vs, _) = typscheme thy (c, raw_ty);
+    val sortargs = case AxClass.class_of_param thy c
+     of SOME class => [[class]]
+      | NONE => (case get_type_of_constr_or_abstr thy c
+         of SOME (tyco, _) => (map snd o fst o the)
+              (AList.lookup (op =) ((snd o fst o get_type thy) tyco) c)
+          | NONE => replicate (length vs) []);
+    val the_sort = the o AList.lookup (op =) (map fst vs ~~ sortargs);
+    val ty = map_type_tfree (fn (v, _) => TFree (v, the_sort v)) raw_ty
     val chead = build_head thy (c, ty);
   in Equations (Thm.weaken chead Drule.dummy_thm, []) end;