# HG changeset patch
# User wenzelm
# Date 1408621589 -7200
# Node ID dc58ab4d9f441ad492534a2de03382f2651263c7
# Parent  83599179e6eb3879a7b4bc8de67a8724b1486328
discontinued odd "temporary" workaround from 2006 (6ac7a4fc32a0), which has no measurable relevance;

diff -r 83599179e6eb -r dc58ab4d9f44 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Thu Aug 21 13:31:31 2014 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Thu Aug 21 13:46:29 2014 +0200
@@ -64,12 +64,6 @@
     val t' = f t;
   in if t aconv t' then NONE else SOME (t, t') end;
 
-val add_used =
-  (Thm.fold_terms o fold_types o fold_atyps)
-    (fn TFree (a, _) => insert (op =) a
-      | TVar ((a, _), _) => insert (op =) a
-      | _ => I);
-
 in
 
 fun read_termTs ctxt ss Ts =
@@ -131,8 +125,7 @@
   let
     val ctxt' = ctxt
       |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2
-      |> Variable.declare_thm thm
-      |> fold (fn a => Variable.declare_names (Logic.mk_type (TFree (a, dummyS)))) (add_used thm []);  (* FIXME !? *)
+      |> Variable.declare_thm thm;
     val tvars = Thm.fold_terms Term.add_tvars thm [];
     val vars = Thm.fold_terms Term.add_vars thm [];
     val insts = read_insts ctxt' mixed_insts (tvars, vars);