1.1 --- a/src/Pure/Isar/code.ML	Sat Sep 22 21:59:40 2012 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Sat Sep 22 21:59:40 2012 +0200
     1.3 @@ -116,6 +116,23 @@
     1.4  
     1.5  (* constants *)
     1.6  
     1.7 +fun const_typ thy = Type.strip_sorts o Sign.the_const_type thy;
     1.8 +
     1.9 +fun args_number thy = length o binder_types o const_typ thy;
    1.10 +
    1.11 +fun devarify ty =
    1.12 +  let
    1.13 +    val tys = fold_atyps (fn TVar vi_sort => AList.update (op =) vi_sort) ty [];
    1.14 +    val vs = Name.invent Name.context Name.aT (length tys);
    1.15 +    val mapping = map2 (fn v => fn (vi, sort) => (vi, TFree (v, sort))) vs tys;
    1.16 +  in Term.typ_subst_TVars mapping ty end;
    1.17 +
    1.18 +fun typscheme thy (c, ty) =
    1.19 +  (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
    1.20 +
    1.21 +fun typscheme_equiv (ty1, ty2) =
    1.22 +  Type.raw_instance (devarify ty1, ty2) andalso Type.raw_instance (devarify ty2, ty1);
    1.23 +
    1.24  fun check_bare_const thy t = case try dest_Const t
    1.25   of SOME c_ty => c_ty
    1.26    | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
    1.27 @@ -125,7 +142,7 @@
    1.28      val c' = AxClass.unoverload_const thy (c, ty);
    1.29      val ty_decl = Sign.the_const_type thy c';
    1.30    in
    1.31 -    if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts (Logic.varifyT_global ty))
    1.32 +    if typscheme_equiv (ty_decl, Logic.varifyT_global ty)
    1.33      then c'
    1.34      else
    1.35        error ("Type\n" ^ string_of_typ thy ty ^
    1.36 @@ -329,18 +346,6 @@
    1.37  
    1.38  (** foundation **)
    1.39  
    1.40 -(* constants *)
    1.41 -
    1.42 -fun const_typ thy = Type.strip_sorts o Sign.the_const_type thy;
    1.43 -
    1.44 -fun args_number thy = length o binder_types o const_typ thy;
    1.45 -
    1.46 -fun logical_typscheme thy (c, ty) =
    1.47 -  (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
    1.48 -
    1.49 -fun typscheme thy (c, ty) = logical_typscheme thy (c, ty);
    1.50 -
    1.51 -
    1.52  (* datatypes *)
    1.53  
    1.54  fun no_constr thy s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c
    1.55 @@ -383,7 +388,7 @@
    1.56        let
    1.57          val the_v = the o AList.lookup (op =) (vs ~~ vs');
    1.58          val ty' = map_type_tfree (fn (v, _) => TFree (the_v v)) ty;
    1.59 -        val (vs'', _) = logical_typscheme thy (c, ty');
    1.60 +        val (vs'', _) = typscheme thy (c, ty');
    1.61        in (c, (vs'', binder_types ty')) end;
    1.62      val c' :: cs' = map (analyze_constructor thy) cs;
    1.63      val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
    1.64 @@ -444,7 +449,7 @@
    1.65  fun check_decl_ty thy (c, ty) =
    1.66    let
    1.67      val ty_decl = Sign.the_const_type thy c;
    1.68 -  in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) then ()
    1.69 +  in if typscheme_equiv (ty_decl, ty) then ()
    1.70      else bad_thm ("Type\n" ^ string_of_typ thy ty
    1.71        ^ "\nof constant " ^ quote c
    1.72        ^ "\nis too specific compared to declared type\n"
    1.73 @@ -647,7 +652,7 @@
    1.74      val ((tyco, sorts), (abs, (vs, ty'))) =
    1.75        analyze_constructor thy (abs, Logic.unvarifyT_global raw_ty);
    1.76      val ty = domain_type ty';
    1.77 -    val (vs', _) = logical_typscheme thy (abs, ty');
    1.78 +    val (vs', _) = typscheme thy (abs, ty');
    1.79    in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
    1.80  
    1.81  
    1.82 @@ -711,7 +716,7 @@
    1.83  fun empty_cert thy c = 
    1.84    let
    1.85      val raw_ty = Logic.unvarifyT_global (const_typ thy c);
    1.86 -    val (vs, _) = logical_typscheme thy (c, raw_ty);
    1.87 +    val (vs, _) = typscheme thy (c, raw_ty);
    1.88      val sortargs = case AxClass.class_of_param thy c
    1.89       of SOME class => [[class]]
    1.90        | NONE => (case get_type_of_constr_or_abstr thy c