Variable.declare_typ;
authorwenzelm
Thu, 19 Jun 2008 20:48:05 +0200
changeset 27281 b457537e789a
parent 27280 2a38802d3649
child 27282 432a5baa7546
Variable.declare_typ;
src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Jun 19 20:48:04 2008 +0200
+++ b/src/Pure/Isar/class.ML	Thu Jun 19 20:48:05 2008 +0200
@@ -747,7 +747,7 @@
     thy
     |> ProofContext.init
     |> Instantiation.put (mk_instantiation ((tycos, vs, sort), inst_params))
-    |> fold (Variable.declare_term o Logic.mk_type o TFree) vs
+    |> fold (Variable.declare_typ o TFree) vs
     |> fold (Variable.declare_names o Free o snd) inst_params
     |> (Overloading.map_improvable_syntax o apfst)
          (fn ((_, _), ((_, subst), unchecks)) =>