# HG changeset patch
# User haftmann
# Date 1497938516 -7200
# Node ID 39e1c876bfec7943e01149bc2a8c9a6ee30be700
# Parent  d0476618a94cf2ed999f31a1b5e417bed541ff3c
more uniform order of constructors

diff -r d0476618a94c -r 39e1c876bfec src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
+++ b/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
@@ -168,11 +168,11 @@
 
 (* functions *)
 
-datatype fun_spec = Eqns_Default of (thm * bool) list * (thm * bool) list lazy
+datatype fun_spec = Unimplemented
+  | Eqns_Default of (thm * bool) list * (thm * bool) list lazy
       (* (cache for default equations, lazy computation of default equations)
          -- helps to restore natural order of default equations *)
   | Eqns of (thm * bool) list
-  | Unimplemented
   | Proj of (term * string) * bool
   | Abstr of (thm * string) * bool;
 
@@ -944,11 +944,11 @@
 
 fun get_cert ctxt functrans c =
   case retrieve_raw (Proof_Context.theory_of ctxt) c of
-    Eqns_Default (_, eqns_lazy) => Lazy.force eqns_lazy
+    Unimplemented => nothing_cert ctxt c
+  | Eqns_Default (_, eqns_lazy) => Lazy.force eqns_lazy
       |> cert_of_eqns_preprocess ctxt functrans c
   | Eqns eqns => eqns
       |> cert_of_eqns_preprocess ctxt functrans c
-  | Unimplemented => nothing_cert ctxt c
   | Proj ((_, tyco), _) => cert_of_proj ctxt c tyco
   | Abstr ((abs_thm, tyco), _) => abs_thm
      |> preprocess Conv.arg_conv ctxt
@@ -1020,10 +1020,12 @@
     fun pretty_equations const thms =
       (Pretty.block o Pretty.fbreaks)
         (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms);
-    fun pretty_function (const, Eqns_Default (_, eqns_lazy)) =
+    fun pretty_function (const, Unimplemented) =
+          pretty_equations const []
+      | pretty_function (const, Eqns_Default (_, eqns_lazy)) =
           pretty_equations const (map fst (Lazy.force eqns_lazy))
-      | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
-      | pretty_function (const, Unimplemented) = pretty_equations const []
+      | pretty_function (const, Eqns eqns) =
+          pretty_equations const (map fst eqns)
       | pretty_function (const, Proj ((proj, _), _)) = Pretty.block
           [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]
       | pretty_function (const, Abstr ((thm, _), _)) = pretty_equations const [thm];
@@ -1124,9 +1126,9 @@
       in (thm, proper) :: filter_out drop eqns end;
     fun natural_order eqns =
       (eqns, Lazy.lazy (fn () => fold (update_subsume false) eqns []))
-    fun add_eqn' true (Eqns_Default (eqns, _)) = Eqns_Default (natural_order ((thm, proper) :: eqns))
+    fun add_eqn' true Unimplemented = Eqns_Default (natural_order [(thm, proper)])
+      | add_eqn' true (Eqns_Default (eqns, _)) = Eqns_Default (natural_order ((thm, proper) :: eqns))
           (*this restores the natural order and drops syntactic redundancies*)
-      | add_eqn' true Unimplemented = Eqns_Default (natural_order [(thm, proper)])
       | add_eqn' true fun_spec = fun_spec
       | add_eqn' false (Eqns eqns) = Eqns (update_subsume true (thm, proper) eqns)
       | add_eqn' false _ = Eqns [(thm, proper)];