more explicit constructor name
authorhaftmann
Tue Jun 20 08:01:56 2017 +0200 (2017-06-20)
changeset 6612660bf6934fabd
parent 66125 28e782dd0278
child 66127 0561ac527270
more explicit constructor name
src/Pure/Isar/code.ML
     1.1 --- a/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
     1.3 @@ -172,7 +172,7 @@
     1.4        (* (cache for default equations, lazy computation of default equations)
     1.5           -- helps to restore natural order of default equations *)
     1.6    | Eqns of (thm * bool) list
     1.7 -  | None
     1.8 +  | Unimplemented
     1.9    | Proj of (term * string) * bool
    1.10    | Abstr of (thm * string) * bool;
    1.11  
    1.12 @@ -909,7 +909,7 @@
    1.13  fun retrieve_raw thy c =
    1.14    Symtab.lookup ((the_functions o the_exec) thy) c
    1.15    |> Option.map (snd o fst)
    1.16 -  |> the_default None
    1.17 +  |> the_default Unimplemented
    1.18  
    1.19  fun eqn_conv conv ct =
    1.20    let
    1.21 @@ -948,7 +948,7 @@
    1.22          |> cert_of_eqns_preprocess ctxt functrans c
    1.23      | Eqns eqns => eqns
    1.24          |> cert_of_eqns_preprocess ctxt functrans c
    1.25 -    | None => nothing_cert ctxt c
    1.26 +    | Unimplemented => nothing_cert ctxt c
    1.27      | Proj ((_, tyco), _) => cert_of_proj thy c tyco
    1.28      | Abstr ((abs_thm, tyco), _) => abs_thm
    1.29         |> preprocess Conv.arg_conv ctxt
    1.30 @@ -1018,7 +1018,7 @@
    1.31      fun pretty_function (const, Eqns_Default (_, eqns_lazy)) =
    1.32            pretty_equations const (map fst (Lazy.force eqns_lazy))
    1.33        | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
    1.34 -      | pretty_function (const, None) = pretty_equations const []
    1.35 +      | pretty_function (const, Unimplemented) = pretty_equations const []
    1.36        | pretty_function (const, Proj ((proj, _), _)) = Pretty.block
    1.37            [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]
    1.38        | pretty_function (const, Abstr ((thm, _), _)) = pretty_equations const [thm];
    1.39 @@ -1121,7 +1121,7 @@
    1.40        (eqns, Lazy.lazy (fn () => fold (update_subsume false) eqns []))
    1.41      fun add_eqn' true (Eqns_Default (eqns, _)) = Eqns_Default (natural_order ((thm, proper) :: eqns))
    1.42            (*this restores the natural order and drops syntactic redundancies*)
    1.43 -      | add_eqn' true None = Eqns_Default (natural_order [(thm, proper)])
    1.44 +      | add_eqn' true Unimplemented = Eqns_Default (natural_order [(thm, proper)])
    1.45        | add_eqn' true fun_spec = fun_spec
    1.46        | add_eqn' false (Eqns eqns) = Eqns (update_subsume true (thm, proper) eqns)
    1.47        | add_eqn' false _ = Eqns [(thm, proper)];
    1.48 @@ -1184,7 +1184,7 @@
    1.49            | del_eqn' (Eqns eqns) =
    1.50                let
    1.51                  val eqns' = filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns
    1.52 -              in if null eqns' then None else Eqns eqns' end
    1.53 +              in if null eqns' then Unimplemented else Eqns eqns' end
    1.54            | del_eqn' spec = spec
    1.55        in change_fun_spec (const_eqn thy thm) del_eqn' thy end
    1.56    | NONE => thy;
    1.57 @@ -1192,7 +1192,7 @@
    1.58  val del_eqn_silent = generic_del_eqn Silent;
    1.59  val del_eqn = generic_del_eqn Liberal;
    1.60  
    1.61 -fun del_eqns c = change_fun_spec c (K None);
    1.62 +fun del_eqns c = change_fun_spec c (K Unimplemented);
    1.63  
    1.64  fun del_exception c = change_fun_spec c (K (Eqns []));
    1.65