src/HOL/Fun.thy
changeset 15531 08c8dad8e399
parent 15510 9de204d7b699
child 15691 900cf45ff0a6
     1.1 --- a/src/HOL/Fun.thy	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Fun.thy	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -474,14 +474,14 @@
     1.4  
     1.5  (* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *)
     1.6  local
     1.7 -  fun gen_fun_upd None T _ _ = None
     1.8 -    | gen_fun_upd (Some f) T x y = Some (Const ("Fun.fun_upd",T) $ f $ x $ y)
     1.9 +  fun gen_fun_upd NONE T _ _ = NONE
    1.10 +    | gen_fun_upd (SOME f) T x y = SOME (Const ("Fun.fun_upd",T) $ f $ x $ y)
    1.11    fun dest_fun_T1 (Type (_, T :: Ts)) = T
    1.12    fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) =
    1.13      let
    1.14        fun find (Const ("Fun.fun_upd",T) $ g $ v $ w) =
    1.15 -            if v aconv x then Some g else gen_fun_upd (find g) T v w
    1.16 -        | find t = None
    1.17 +            if v aconv x then SOME g else gen_fun_upd (find g) T v w
    1.18 +        | find t = NONE
    1.19      in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
    1.20  
    1.21    val ss = simpset ()
    1.22 @@ -491,8 +491,8 @@
    1.23      Simplifier.simproc (Theory.sign_of (the_context ()))
    1.24        "fun_upd2" ["f(v := w, x := y)"]
    1.25        (fn sg => fn _ => fn t =>
    1.26 -        case find_double t of (T, None) => None
    1.27 -        | (T, Some rhs) => Some (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) fun_upd_prover))
    1.28 +        case find_double t of (T, NONE) => NONE
    1.29 +        | (T, SOME rhs) => SOME (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) fun_upd_prover))
    1.30  end;
    1.31  Addsimprocs[fun_upd2_simproc];
    1.32