diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/HOL/Library/reflection.ML
--- a/src/HOL/Library/reflection.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/HOL/Library/reflection.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -34,7 +34,7 @@
      |> fst |> strip_comb |> fst
    val thy = ProofContext.theory_of ctxt
    val cert = Thm.cterm_of thy
-   val (((_,_),[th']), ctxt') = Variable.import_thms true [th] ctxt
+   val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt
    val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))
    fun add_fterms (t as t1 $ t2) =
        if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t