# HG changeset patch
# User wenzelm
# Date 1213901285 -7200
# Node ID b457537e789ab10840ba4d82fa36ff746f688dd2
# Parent  2a38802d3649f089ea6d02cdcaa45a68ccc401aa
Variable.declare_typ;

diff -r 2a38802d3649 -r b457537e789a 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)) =>