read_instantiate: declare names of TVars as well (temporary workaround for no-freeze feature of type inference);
authorwenzelm
Wed Sep 06 22:48:36 2006 +0200 (2006-09-06)
changeset 204876ac7a4fc32a0
parent 20486 02ca20e33030
child 20488 121bc2135bd3
read_instantiate: declare names of TVars as well (temporary workaround for no-freeze feature of type inference);
src/Pure/Isar/rule_insts.ML
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Wed Sep 06 17:39:52 2006 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Wed Sep 06 22:48:36 2006 +0200
     1.3 @@ -129,7 +129,8 @@
     1.4  
     1.5  fun read_instantiate ctxt mixed_insts thm =
     1.6    let
     1.7 -    val ctxt' = ctxt |> Variable.declare_thm thm;
     1.8 +    val ctxt' = ctxt |> Variable.declare_thm thm
     1.9 +      |> fold (fn a => Variable.declare_internal (Logic.mk_type (TFree (a, [])))) (Drule.add_used thm []);  (* FIXME tmp *)
    1.10      val tvars = Drule.fold_terms Term.add_tvars thm [];
    1.11      val vars = Drule.fold_terms Term.add_vars thm [];
    1.12      val ((type_insts, term_insts), insts) = read_insts ctxt' (map snd mixed_insts) (tvars, vars);