Variable.declare_typ;
authorwenzelm
Thu, 19 Jun 2008 20:48:05 +0200
changeset 27281b457537e789a
parent 27280 2a38802d3649
child 27282 432a5baa7546
Variable.declare_typ;
src/Pure/Isar/class.ML
     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)) =>