more uniform order of constructors
authorhaftmann
Tue Jun 20 08:01:56 2017 +0200 (2017-06-20)
changeset 6613139e1c876bfec
parent 66130 d0476618a94c
child 66132 5844a096c462
more uniform order of constructors
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 @@ -168,11 +168,11 @@
     1.4  
     1.5  (* functions *)
     1.6  
     1.7 -datatype fun_spec = Eqns_Default of (thm * bool) list * (thm * bool) list lazy
     1.8 +datatype fun_spec = Unimplemented
     1.9 +  | Eqns_Default of (thm * bool) list * (thm * bool) list lazy
    1.10        (* (cache for default equations, lazy computation of default equations)
    1.11           -- helps to restore natural order of default equations *)
    1.12    | Eqns of (thm * bool) list
    1.13 -  | Unimplemented
    1.14    | Proj of (term * string) * bool
    1.15    | Abstr of (thm * string) * bool;
    1.16  
    1.17 @@ -944,11 +944,11 @@
    1.18  
    1.19  fun get_cert ctxt functrans c =
    1.20    case retrieve_raw (Proof_Context.theory_of ctxt) c of
    1.21 -    Eqns_Default (_, eqns_lazy) => Lazy.force eqns_lazy
    1.22 +    Unimplemented => nothing_cert ctxt c
    1.23 +  | Eqns_Default (_, eqns_lazy) => Lazy.force eqns_lazy
    1.24        |> cert_of_eqns_preprocess ctxt functrans c
    1.25    | Eqns eqns => eqns
    1.26        |> cert_of_eqns_preprocess ctxt functrans c
    1.27 -  | Unimplemented => nothing_cert ctxt c
    1.28    | Proj ((_, tyco), _) => cert_of_proj ctxt c tyco
    1.29    | Abstr ((abs_thm, tyco), _) => abs_thm
    1.30       |> preprocess Conv.arg_conv ctxt
    1.31 @@ -1020,10 +1020,12 @@
    1.32      fun pretty_equations const thms =
    1.33        (Pretty.block o Pretty.fbreaks)
    1.34          (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms);
    1.35 -    fun pretty_function (const, Eqns_Default (_, eqns_lazy)) =
    1.36 +    fun pretty_function (const, Unimplemented) =
    1.37 +          pretty_equations const []
    1.38 +      | pretty_function (const, Eqns_Default (_, eqns_lazy)) =
    1.39            pretty_equations const (map fst (Lazy.force eqns_lazy))
    1.40 -      | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
    1.41 -      | pretty_function (const, Unimplemented) = pretty_equations const []
    1.42 +      | pretty_function (const, Eqns eqns) =
    1.43 +          pretty_equations const (map fst eqns)
    1.44        | pretty_function (const, Proj ((proj, _), _)) = Pretty.block
    1.45            [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]
    1.46        | pretty_function (const, Abstr ((thm, _), _)) = pretty_equations const [thm];
    1.47 @@ -1124,9 +1126,9 @@
    1.48        in (thm, proper) :: filter_out drop eqns end;
    1.49      fun natural_order eqns =
    1.50        (eqns, Lazy.lazy (fn () => fold (update_subsume false) eqns []))
    1.51 -    fun add_eqn' true (Eqns_Default (eqns, _)) = Eqns_Default (natural_order ((thm, proper) :: eqns))
    1.52 +    fun add_eqn' true Unimplemented = Eqns_Default (natural_order [(thm, proper)])
    1.53 +      | add_eqn' true (Eqns_Default (eqns, _)) = Eqns_Default (natural_order ((thm, proper) :: eqns))
    1.54            (*this restores the natural order and drops syntactic redundancies*)
    1.55 -      | add_eqn' true Unimplemented = Eqns_Default (natural_order [(thm, proper)])
    1.56        | add_eqn' true fun_spec = fun_spec
    1.57        | add_eqn' false (Eqns eqns) = Eqns (update_subsume true (thm, proper) eqns)
    1.58        | add_eqn' false _ = Eqns [(thm, proper)];