src/Pure/axclass.ML
changeset 21893 29438dfa8a16
parent 21687 f689f729afab
child 21913 1224048fb8f9
     1.1 --- a/src/Pure/axclass.ML	Thu Dec 21 13:55:12 2006 +0100
     1.2 +++ b/src/Pure/axclass.ML	Thu Dec 21 13:55:13 2006 +0100
     1.3 @@ -340,10 +340,10 @@
     1.4      val params_typs = map (fn param =>
     1.5        let
     1.6          val ty = Sign.the_const_type thy param;
     1.7 -        val var = case Term.typ_tvars ty
     1.8 -         of [(v, _)] => v
     1.9 +        val _ = case Term.typ_tvars ty
    1.10 +         of [_] => ()
    1.11            | _ => error ("exactly one type variable required in parameter " ^ quote param);
    1.12 -        val ty' = Term.typ_subst_TVars [(var, TFree (param_tyvarname, []))] ty;
    1.13 +        val ty' = Term.map_type_tvar (fn _ => TFree (param_tyvarname, [class])) ty;
    1.14        in (param, ty') end) params;
    1.15      val operational = length params_typs > 0 orelse
    1.16        length (filter (the_default false o Option.map