src/HOL/Tools/SMT/smt_normalize.ML
changeset 37153 8feed34275ce
parent 36936 c52d1c130898
child 37786 4eb98849c5c0
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu May 27 14:58:45 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu May 27 16:29:33 2010 +0200
     1.3 @@ -391,7 +391,7 @@
     1.4    fun abs_conv conv tb = Conv.abs_conv (fn (cv, cx) =>
     1.5      let val n = fst (Term.dest_Free (Thm.term_of cv))
     1.6      in conv (Symtab.update (free n, 0) tb) cx end)
     1.7 -  val apply_rule = @{lemma "f x == apply f x" by (simp add: apply_def)}
     1.8 +  val fun_app_rule = @{lemma "f x == fun_app f x" by (simp add: fun_app_def)}
     1.9  in
    1.10  fun explicit_application ctxt thms =
    1.11    let
    1.12 @@ -404,12 +404,12 @@
    1.13      and app_conv tb n i ctxt =
    1.14        (case Symtab.lookup tb n of
    1.15          NONE => nary_conv Conv.all_conv (sub_conv tb ctxt)
    1.16 -      | SOME j => apply_conv tb ctxt (i - j))
    1.17 -    and apply_conv tb ctxt i ct = (
    1.18 +      | SOME j => fun_app_conv tb ctxt (i - j))
    1.19 +    and fun_app_conv tb ctxt i ct = (
    1.20        if i = 0 then nary_conv Conv.all_conv (sub_conv tb ctxt)
    1.21        else
    1.22 -        Conv.rewr_conv apply_rule then_conv
    1.23 -        binop_conv (apply_conv tb ctxt (i-1)) (sub_conv tb ctxt)) ct
    1.24 +        Conv.rewr_conv fun_app_rule then_conv
    1.25 +        binop_conv (fun_app_conv tb ctxt (i-1)) (sub_conv tb ctxt)) ct
    1.26  
    1.27      fun needs_exp_app tab = Term.exists_subterm (fn
    1.28          Bound _ $ _ => true