src/HOL/Extraction.thy
changeset 15531 08c8dad8e399
parent 15393 2e6a9146caca
child 16121 a80aa66d2271
     1.1 --- a/src/HOL/Extraction.thy	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Extraction.thy	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -15,19 +15,19 @@
     1.4  ML_setup {*
     1.5  fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $
     1.6        (Const ("op :", _) $ x $ S)) = (case strip_comb S of
     1.7 -        (Var (ixn, U), ts) => Some (list_comb (Var (ixn, binder_types U @
     1.8 +        (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, binder_types U @
     1.9             [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), ts @ [x]))
    1.10 -      | (Free (s, U), ts) => Some (list_comb (Free (s, binder_types U @
    1.11 +      | (Free (s, U), ts) => SOME (list_comb (Free (s, binder_types U @
    1.12             [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), ts @ [x]))
    1.13 -      | _ => None)
    1.14 +      | _ => NONE)
    1.15    | realizes_set_proc (Const ("realizes", Type ("fun", [T, _])) $ r $
    1.16        (Const ("op :", _) $ x $ S)) = (case strip_comb S of
    1.17 -        (Var (ixn, U), ts) => Some (list_comb (Var (ixn, T :: binder_types U @
    1.18 +        (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, T :: binder_types U @
    1.19             [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), r :: ts @ [x]))
    1.20 -      | (Free (s, U), ts) => Some (list_comb (Free (s, T :: binder_types U @
    1.21 +      | (Free (s, U), ts) => SOME (list_comb (Free (s, T :: binder_types U @
    1.22             [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), r :: ts @ [x]))
    1.23 -      | _ => None)
    1.24 -  | realizes_set_proc _ = None;
    1.25 +      | _ => NONE)
    1.26 +  | realizes_set_proc _ = NONE;
    1.27  
    1.28  fun mk_realizes_set r rT s (setT as Type ("set", [elT])) =
    1.29    Abs ("x", elT, Const ("realizes", rT --> HOLogic.boolT --> HOLogic.boolT) $
    1.30 @@ -36,8 +36,8 @@
    1.31  
    1.32    Context.>> (fn thy => thy |>
    1.33      Extraction.add_types
    1.34 -      [("bool", ([], None)),
    1.35 -       ("set", ([realizes_set_proc], Some mk_realizes_set))] |>
    1.36 +      [("bool", ([], NONE)),
    1.37 +       ("set", ([realizes_set_proc], SOME mk_realizes_set))] |>
    1.38      Extraction.set_preprocessor (fn sg =>
    1.39        Proofterm.rewrite_proof_notypes
    1.40          ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::