--- 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