tuned;
authorwenzelm
Wed Oct 31 14:47:59 2018 +0100 (6 months ago)
changeset 6921474455459973d
parent 69213 ab98f058f9dc
child 69215 ab94035ba6ea
tuned;
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
     1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Tue Oct 30 22:59:06 2018 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Oct 31 14:47:59 2018 +0100
     1.3 @@ -2507,12 +2507,12 @@
     1.4      (case t of
     1.5        (l as f $ a) $ b =>
     1.6          if is_ty t orelse is_op t then term_bools (term_bools acc l) b
     1.7 -        else insert (aconv) t acc
     1.8 +        else insert (op aconv) t acc
     1.9      | f $ a =>
    1.10          if is_ty t orelse is_op t then term_bools (term_bools acc f) a
    1.11 -        else insert (aconv) t acc
    1.12 +        else insert (op aconv) t acc
    1.13      | Abs p => term_bools acc (snd (Syntax_Trans.variant_abs p))  (* FIXME !? *)
    1.14 -    | _ => if is_ty t orelse is_op t then acc else insert (aconv) t acc)
    1.15 +    | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc)
    1.16    end;
    1.17  
    1.18  in
     2.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Oct 30 22:59:06 2018 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Oct 31 14:47:59 2018 +0100
     2.3 @@ -4066,7 +4066,7 @@
     2.4  fun frpar_procedure alternative T ps fm =
     2.5    let
     2.6      val frpar = if alternative then @{code frpar2} else @{code frpar};
     2.7 -    val fs = subtract (aconv) (map Free (Term.add_frees fm [])) ps;
     2.8 +    val fs = subtract (op aconv) (map Free (Term.add_frees fm [])) ps;
     2.9      val eval = term_of_fm T fs ps o frpar o fm_of_term fs ps;
    2.10      val t = HOLogic.dest_Trueprop fm;
    2.11    in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, eval t)) end;