src/Pure/Isar/rule_insts.ML
changeset 27282 432a5baa7546
parent 27245 817d34377170
child 27378 0968c0d0b969
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Thu Jun 19 20:48:05 2008 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu Jun 19 20:48:06 2008 +0200
     1.3 @@ -69,6 +69,12 @@
     1.4      val t' = f t;
     1.5    in if t aconv t' then NONE else SOME (t, t') end;
     1.6  
     1.7 +val add_used =
     1.8 +  (Thm.fold_terms o fold_types o fold_atyps)
     1.9 +    (fn TFree (a, _) => insert (op =) a
    1.10 +      | TVar ((a, _), _) => insert (op =) a
    1.11 +      | _ => I);
    1.12 +
    1.13  in
    1.14  
    1.15  fun read_termTs ctxt schematic ss Ts =
    1.16 @@ -155,7 +161,7 @@
    1.17  fun read_instantiate_mixed ctxt mixed_insts thm =
    1.18    let
    1.19      val ctxt' = ctxt |> Variable.declare_thm thm
    1.20 -      |> fold (fn a => Variable.declare_internal (Logic.mk_type (TFree (a, [])))) (Drule.add_used thm []);  (* FIXME tmp *)
    1.21 +      |> fold (fn a => Variable.declare_names (Logic.mk_type (TFree (a, dummyS)))) (add_used thm []);  (* FIXME tmp *)
    1.22      val tvars = Thm.fold_terms Term.add_tvars thm [];
    1.23      val vars = Thm.fold_terms Term.add_vars thm [];
    1.24      val ((type_insts, term_insts), insts) = read_insts ctxt' (map snd mixed_insts) (tvars, vars);