# HG changeset patch
# User haftmann
# Date 1166705713 -3600
# Node ID 29438dfa8a169a624050ee79a6ac17e474a20882
# Parent  af35b480916e7841d53fba351eda126a8480e98e
code clarifications

diff -r af35b480916e -r 29438dfa8a16 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Thu Dec 21 13:55:12 2006 +0100
+++ b/src/Pure/axclass.ML	Thu Dec 21 13:55:13 2006 +0100
@@ -340,10 +340,10 @@
     val params_typs = map (fn param =>
       let
         val ty = Sign.the_const_type thy param;
-        val var = case Term.typ_tvars ty
-         of [(v, _)] => v
+        val _ = case Term.typ_tvars ty
+         of [_] => ()
           | _ => error ("exactly one type variable required in parameter " ^ quote param);
-        val ty' = Term.typ_subst_TVars [(var, TFree (param_tyvarname, []))] ty;
+        val ty' = Term.map_type_tvar (fn _ => TFree (param_tyvarname, [class])) ty;
       in (param, ty') end) params;
     val operational = length params_typs > 0 orelse
       length (filter (the_default false o Option.map