src/HOL/Library/reflection.ML
changeset 31794 71af1fd6a5e4
parent 31412 f2e6b6526092
child 31810 a6b800855cdd
     1.1 --- a/src/HOL/Library/reflection.ML	Wed Jun 24 20:52:49 2009 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Wed Jun 24 21:28:02 2009 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4       |> fst |> strip_comb |> fst
     1.5     val thy = ProofContext.theory_of ctxt
     1.6     val cert = Thm.cterm_of thy
     1.7 -   val (((_,_),[th']), ctxt') = Variable.import_thms true [th] ctxt
     1.8 +   val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt
     1.9     val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))
    1.10     fun add_fterms (t as t1 $ t2) =
    1.11         if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t