# HG changeset patch
# User wenzelm
# Date 1157575716 -7200
# Node ID 6ac7a4fc32a0a0593e83c0e77b9287e4f8a5ba5b
# Parent  02ca20e33030f346dc5133c265268a93530eecb4
read_instantiate: declare names of TVars as well (temporary workaround for no-freeze feature of type inference);

diff -r 02ca20e33030 -r 6ac7a4fc32a0 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Wed Sep 06 17:39:52 2006 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Wed Sep 06 22:48:36 2006 +0200
@@ -129,7 +129,8 @@
 
 fun read_instantiate ctxt mixed_insts thm =
   let
-    val ctxt' = ctxt |> Variable.declare_thm thm;
+    val ctxt' = ctxt |> Variable.declare_thm thm
+      |> fold (fn a => Variable.declare_internal (Logic.mk_type (TFree (a, [])))) (Drule.add_used thm []);  (* FIXME tmp *)
     val tvars = Drule.fold_terms Term.add_tvars thm [];
     val vars = Drule.fold_terms Term.add_vars thm [];
     val ((type_insts, term_insts), insts) = read_insts ctxt' (map snd mixed_insts) (tvars, vars);