32 let |
32 let |
33 val (f as Const(fN,fT)) = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |
33 val (f as Const(fN,fT)) = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |
34 |> fst |> strip_comb |> fst |
34 |> fst |> strip_comb |> fst |
35 val thy = ProofContext.theory_of ctxt |
35 val thy = ProofContext.theory_of ctxt |
36 val cert = Thm.cterm_of thy |
36 val cert = Thm.cterm_of thy |
37 val (((_,_),[th']), ctxt') = Variable.import_thms true [th] ctxt |
37 val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt |
38 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th')) |
38 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th')) |
39 fun add_fterms (t as t1 $ t2) = |
39 fun add_fterms (t as t1 $ t2) = |
40 if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t |
40 if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t |
41 else add_fterms t1 #> add_fterms t2 |
41 else add_fterms t1 #> add_fterms t2 |
42 | add_fterms (t as Abs(xn,xT,t')) = |
42 | add_fterms (t as Abs(xn,xT,t')) = |