src/Pure/Isar/class.ML
changeset 27281 b457537e789a
parent 27089 480f19078b65
child 27684 f45fd1159a4b
     1.1 --- a/src/Pure/Isar/class.ML	Thu Jun 19 20:48:04 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Jun 19 20:48:05 2008 +0200
     1.3 @@ -747,7 +747,7 @@
     1.4      thy
     1.5      |> ProofContext.init
     1.6      |> Instantiation.put (mk_instantiation ((tycos, vs, sort), inst_params))
     1.7 -    |> fold (Variable.declare_term o Logic.mk_type o TFree) vs
     1.8 +    |> fold (Variable.declare_typ o TFree) vs
     1.9      |> fold (Variable.declare_names o Free o snd) inst_params
    1.10      |> (Overloading.map_improvable_syntax o apfst)
    1.11           (fn ((_, _), ((_, subst), unchecks)) =>