src/HOL/ex/reflection.ML
changeset 29273 285c00993bc2
parent 29269 5c25a2012975
equal deleted inserted replaced
29272:fb3ccf499df5 29273:285c00993bc2
    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')) = 
    43        if (fN mem (term_consts t)) then (fn _ => [t]) else (fn _ => [])
    43        if exists_Const (fn (c, _) => c = fN) t then (fn _ => [t]) else (fn _ => [])
    44      | add_fterms _ = I
    44      | add_fterms _ = I
    45    val fterms = add_fterms rhs []
    45    val fterms = add_fterms rhs []
    46    val (xs, ctxt'') = Variable.variant_fixes (replicate (length fterms) "x") ctxt'
    46    val (xs, ctxt'') = Variable.variant_fixes (replicate (length fterms) "x") ctxt'
    47    val tys = map fastype_of fterms
    47    val tys = map fastype_of fterms
    48    val vs = map Free (xs ~~ tys)
    48    val vs = map Free (xs ~~ tys)