1.1 --- a/src/Pure/Isar/code.ML	Sat Nov 27 19:41:37 2010 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Sat Nov 27 22:01:27 2010 +0100
     1.3 @@ -358,6 +358,8 @@
     1.4   of SOME ty => ty
     1.5    | NONE => (Type.strip_sorts o Sign.the_const_type thy) c;
     1.6  
     1.7 +fun args_number thy = length o fst o strip_type o const_typ thy;
     1.8 +
     1.9  fun subst_signature thy c ty =
    1.10    let
    1.11      fun mk_subst (Type (_, tys1)) (Type (_, tys2)) =
    1.12 @@ -370,7 +372,10 @@
    1.13  
    1.14  fun subst_signatures thy = map_aterms (fn Const (c, ty) => Const (c, subst_signature thy c ty) | t => t);
    1.15  
    1.16 -fun args_number thy = length o fst o strip_type o const_typ thy;
    1.17 +fun logical_typscheme thy (c, ty) =
    1.18 +  (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
    1.19 +
    1.20 +fun typscheme thy (c, ty) = logical_typscheme thy (c, subst_signature thy c ty);
    1.21  
    1.22  
    1.23  (* datatypes *)
    1.24 @@ -414,7 +419,7 @@
    1.25        let
    1.26          val the_v = the o AList.lookup (op =) (vs ~~ vs');
    1.27          val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty;
    1.28 -        val vs'' = map dest_TFree (Sign.const_typargs thy (c, ty'));
    1.29 +        val (vs'', _) = logical_typscheme thy (c, ty');
    1.30        in (c, (vs'', (fst o strip_type) ty')) end;
    1.31      val c' :: cs' = map (ty_sorts thy) cs;
    1.32      val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
    1.33 @@ -593,11 +598,6 @@
    1.34  fun const_abs_eqn thy = AxClass.unoverload_const thy o dest_Const o fst o strip_comb o snd
    1.35    o dest_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
    1.36  
    1.37 -fun logical_typscheme thy (c, ty) =
    1.38 -  (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
    1.39 -
    1.40 -fun typscheme thy (c, ty) = logical_typscheme thy (c, subst_signature thy c ty);
    1.41 -
    1.42  fun mk_proj tyco vs ty abs rep =
    1.43    let
    1.44      val ty_abs = Type (tyco, map TFree vs);
    1.45 @@ -678,7 +678,7 @@
    1.46      val _ = if param = rhs then () else bad "Not an abstype certificate";
    1.47      val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty);
    1.48      val ty = domain_type ty';
    1.49 -    val vs' = map dest_TFree (Sign.const_typargs thy (abs, ty'));
    1.50 +    val (vs', _) = logical_typscheme thy (abs, ty');
    1.51    in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
    1.52  
    1.53  
    1.54 @@ -743,7 +743,7 @@
    1.55  fun empty_cert thy c = 
    1.56    let
    1.57      val raw_ty = Logic.unvarifyT_global (const_typ thy c);
    1.58 -    val (vs, _) = typscheme thy (c, raw_ty);
    1.59 +    val (vs, _) = logical_typscheme thy (c, raw_ty);
    1.60      val sortargs = case AxClass.class_of_param thy c
    1.61       of SOME class => [[class]]
    1.62        | NONE => (case get_type_of_constr_or_abstr thy c