# HG changeset patch
# User wenzelm
# Date 1497972689 -7200
# Node ID 8f1cbb77a70a1b14d4b1f306abbaf8c0a89b0a16
# Parent  dd006934a7195d982ce4c0573bd419665b8f4e17# Parent  51f74025a3e366da2e7d0352ff710e6ce06485ae
merged

diff -r 51f74025a3e3 -r 8f1cbb77a70a NEWS
--- a/NEWS	Tue Jun 20 17:28:17 2017 +0200
+++ b/NEWS	Tue Jun 20 17:31:29 2017 +0200
@@ -162,7 +162,9 @@
 * Session HOL-Algebra extended by additional lattice theory: the
 Knaster-Tarski fixed point theorem and Galois Connections.
 
-* SMT module: The legacy module 'src/HOL/Library/Old_SMT.thy' has been removed.
+* SMT module:
+  - The legacy module 'src/HOL/Library/Old_SMT.thy' has been removed.
+  - Several small issues have been rectified in the 'smt' command.
 
 * Session HOL-Analysis: more material involving arcs, paths, covering
 spaces, innessential maps, retracts. Major results include the Jordan
diff -r 51f74025a3e3 -r 8f1cbb77a70a src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Tue Jun 20 17:28:17 2017 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Tue Jun 20 17:31:29 2017 +0200
@@ -210,32 +210,33 @@
 | "Ifm bs (E p) = (\<exists> x. Ifm (x#bs) p)"
 | "Ifm bs (A p) = (\<forall> x. Ifm (x#bs) p)"
 
-consts prep :: "fm \<Rightarrow> fm"
-recdef prep "measure fmsize"
+function (sequential) prep :: "fm \<Rightarrow> fm" where
   "prep (E T) = T"
-  "prep (E F) = F"
-  "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
-  "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))"
-  "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
-  "prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))"
-  "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
-  "prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
-  "prep (E p) = E (prep p)"
-  "prep (A (And p q)) = And (prep (A p)) (prep (A q))"
-  "prep (A p) = prep (NOT (E (NOT p)))"
-  "prep (NOT (NOT p)) = prep p"
-  "prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))"
-  "prep (NOT (A p)) = prep (E (NOT p))"
-  "prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))"
-  "prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))"
-  "prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))"
-  "prep (NOT p) = NOT (prep p)"
-  "prep (Or p q) = Or (prep p) (prep q)"
-  "prep (And p q) = And (prep p) (prep q)"
-  "prep (Imp p q) = prep (Or (NOT p) q)"
-  "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
-  "prep p = p"
-(hints simp add: fmsize_pos)
+| "prep (E F) = F"
+| "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
+| "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))"
+| "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
+| "prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))"
+| "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
+| "prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
+| "prep (E p) = E (prep p)"
+| "prep (A (And p q)) = And (prep (A p)) (prep (A q))"
+| "prep (A p) = prep (NOT (E (NOT p)))"
+| "prep (NOT (NOT p)) = prep p"
+| "prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))"
+| "prep (NOT (A p)) = prep (E (NOT p))"
+| "prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))"
+| "prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))"
+| "prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))"
+| "prep (NOT p) = NOT (prep p)"
+| "prep (Or p q) = Or (prep p) (prep q)"
+| "prep (And p q) = And (prep p) (prep q)"
+| "prep (Imp p q) = prep (Or (NOT p) q)"
+| "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
+| "prep p = p"
+  by pat_completeness simp_all
+termination by (relation "measure fmsize") (simp_all add: fmsize_pos)
+
 lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
   by (induct p rule: prep.induct) auto
 
@@ -2239,7 +2240,7 @@
 lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)" by auto
 
 consts
-  a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
+  a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coefficients of a formula *)
   d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
   \<zeta>  :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
   \<beta> :: "fm \<Rightarrow> num list"
diff -r 51f74025a3e3 -r 8f1cbb77a70a src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Jun 20 17:28:17 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Jun 20 17:31:29 2017 +0200
@@ -12,7 +12,6 @@
   datatype sterm =
     SVar of int |
     SApp of string * sterm list |
-    SLet of string * sterm * sterm |
     SQua of squant * string list * sterm spattern list * sterm
 
   (*translation configuration*)
@@ -47,12 +46,12 @@
 
 datatype squant = SForall | SExists
 
-datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
+datatype 'a spattern =
+  SPat of 'a list | SNoPat of 'a list
 
 datatype sterm =
   SVar of int |
   SApp of string * sterm list |
-  SLet of string * sterm * sterm |
   SQua of squant * string list * sterm spattern list * sterm
 
 
@@ -204,7 +203,6 @@
       | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a
       | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp expand T t
       | expand (q as Const (@{const_name Ex}, T)) = exp2 T q
-      | expand (Const (@{const_name Let}, _) $ t $ u) = expand (Term.betapply (u, t))
       | expand (Const (@{const_name Let}, T) $ t) =
           let val U = Term.domain_type (Term.range_type T)
           in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end
@@ -213,7 +211,9 @@
           in Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U, Bound 0 $ Bound 1)) end
       | expand t =
           (case Term.strip_comb t of
-            (u as Const (c as (_, T)), ts) =>
+            (Const (@{const_name Let}, _), t1 :: t2 :: ts) =>
+            Term.betapplys (Term.betapply (expand t2, expand t1), map expand ts)
+          | (u as Const (c as (_, T)), ts) =>
               (case SMT_Builtin.dest_builtin ctxt c ts of
                 SOME (_, k, us, mk) =>
                   if k = length us then mk (map expand us)
@@ -438,8 +438,6 @@
               fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
               trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b'))
           | NONE => raise TERM ("unsupported quantifier", [t]))
-      | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
-          transT T ##>> trans t1 ##>> trans t2 #>> (fn ((U, u1), u2) => SLet (U, u1, u2))
       | (u as Const (c as (_, T)), ts) =>
           (case builtin ctxt c ts of
             SOME (n, _, us, _) => fold_map trans us #>> app n
@@ -516,7 +514,6 @@
 
     val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
       |>> apfst (cons fun_app_eq)
-val _ = dtyps : (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list (*###*)
   in
     (ts4, tr_context)
     |-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
diff -r 51f74025a3e3 -r 8f1cbb77a70a src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Jun 20 17:28:17 2017 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Jun 20 17:31:29 2017 +0200
@@ -94,8 +94,6 @@
   | tree_of_sterm _ (SMT_Translate.SApp (n, [])) = SMTLIB.Sym n
   | tree_of_sterm l (SMT_Translate.SApp (n, ts)) =
       SMTLIB.S (SMTLIB.Sym n :: map (tree_of_sterm l) ts)
-  | tree_of_sterm _ (SMT_Translate.SLet _) =
-      raise Fail "SMT-LIB: unsupported let expression"
   | tree_of_sterm l (SMT_Translate.SQua (q, ss, pats, t)) =
       let
         val l' = l + length ss
diff -r 51f74025a3e3 -r 8f1cbb77a70a src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Jun 20 17:28:17 2017 +0200
+++ b/src/Pure/Isar/code.ML	Tue Jun 20 17:31:29 2017 +0200
@@ -165,17 +165,18 @@
 fun case_consts_of (Constructors (_, case_consts)) = case_consts
   | case_consts_of (Abstractor _) = [];
 
+
 (* 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
-  | None
   | Proj of (term * string) * bool
   | Abstr of (thm * string) * bool;
 
-val initial_fun_spec = Eqns_Default ([], Lazy.value []);
+val default_fun_spec = Eqns_Default ([], Lazy.value []);
 
 fun is_default (Eqns_Default _) = true
   | is_default (Proj (_, default)) = default
@@ -190,9 +191,9 @@
 
 datatype spec = Spec of {
   history_concluded: bool,
-  functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table
+  types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
     (*with explicit history*),
-  types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
+  functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table
     (*with explicit history*),
   cases: ((int * (int * string option list)) * thm) Symtab.table,
   undefineds: unit Symtab.table
@@ -201,6 +202,8 @@
 fun make_spec (history_concluded, (functions, (types, (cases, undefineds)))) =
   Spec { history_concluded = history_concluded, functions = functions, types = types,
     cases = cases, undefineds = undefineds };
+val empty_spec =
+  make_spec (false, (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty))));
 fun map_spec f (Spec { history_concluded = history_concluded,
   functions = functions, types = types, cases = cases, undefineds = undefineds }) =
   make_spec (f (history_concluded, (functions, (types, (cases, undefineds)))));
@@ -224,20 +227,20 @@
     val invalidated_case_consts = union (op =) (case_consts_of' types1) (case_consts_of' types2)
       |> subtract (op =) (maps case_consts_of all_datatype_specs)
     val functions = Symtab.join (K merge_functions) (functions1, functions2)
-      |> fold (fn c => Symtab.map_entry c (apfst (K (true, initial_fun_spec)))) all_constructors;
+      |> fold (fn c => Symtab.map_entry c (apfst (K (true, default_fun_spec)))) all_constructors;
     val cases = Symtab.merge (K true) (cases1, cases2)
       |> fold Symtab.delete invalidated_case_consts;
     val undefineds = Symtab.merge (K true) (undefineds1, undefineds2);
   in make_spec (false, (functions, (types, (cases, undefineds)))) end;
 
 fun history_concluded (Spec { history_concluded, ... }) = history_concluded;
-fun the_functions (Spec { functions, ... }) = functions;
-fun the_types (Spec { types, ... }) = types;
-fun the_cases (Spec { cases, ... }) = cases;
-fun the_undefineds (Spec { undefineds, ... }) = undefineds;
+fun types_of (Spec { types, ... }) = types;
+fun functions_of (Spec { functions, ... }) = functions;
+fun cases_of (Spec { cases, ... }) = cases;
+fun undefineds_of (Spec { undefineds, ... }) = undefineds;
 val map_history_concluded = map_spec o apfst;
 val map_functions = map_spec o apsnd o apfst;
-val map_typs = map_spec o apsnd o apsnd o apfst;
+val map_types = map_spec o apsnd o apsnd o apfst;
 val map_cases = map_spec o apsnd o apsnd o apsnd o apfst;
 val map_undefineds = map_spec o apsnd o apsnd o apsnd o apsnd;
 
@@ -282,8 +285,7 @@
 structure Code_Data = Theory_Data
 (
   type T = spec * (data * theory) option Synchronized.var;
-  val empty = (make_spec (false, (Symtab.empty,
-    (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ());
+  val empty = (empty_spec, empty_dataref ());
   val extend : T -> T = apsnd (K (empty_dataref ()));
   fun merge ((spec1, _), (spec2, _)) =
     (merge_spec (spec1, spec2), empty_dataref ());
@@ -294,24 +296,24 @@
 
 (* access to executable code *)
 
-val the_exec : theory -> spec = fst o Code_Data.get;
+val spec_of : theory -> spec = fst o Code_Data.get;
 
-fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));
+fun map_spec_purge f = Code_Data.map (fn (spec, _) => (f spec, empty_dataref ()));
 
-fun change_fun_spec c f = (map_exec_purge o map_functions
-  o (Symtab.map_default (c, ((false, initial_fun_spec), [])))
+fun change_fun_spec c f = (map_spec_purge o map_functions
+  o (Symtab.map_default (c, ((false, default_fun_spec), [])))
     o apfst) (fn (_, spec) => (true, f spec));
 
 
 (* tackling equation history *)
 
-fun continue_history thy = if (history_concluded o the_exec) thy
+fun continue_history thy = if (history_concluded o spec_of) thy
   then thy
     |> (Code_Data.map o apfst o map_history_concluded) (K false)
     |> SOME
   else NONE;
 
-fun conclude_history thy = if (history_concluded o the_exec) thy
+fun conclude_history thy = if (history_concluded o spec_of) thy
   then NONE
   else thy
     |> (Code_Data.map o apfst)
@@ -349,7 +351,7 @@
 
 (** foundation **)
 
-(* datatypes *)
+(* types *)
 
 fun no_constr thy s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c
   ^ " :: " ^ string_of_typ thy ty ^ "\n" ^ enclose "(" ")" s);
@@ -394,7 +396,7 @@
     val constructors = map (inst vs o snd) raw_constructors;
   in (tyco, (map (rpair []) vs, constructors)) end;
 
-fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
+fun get_type_entry thy tyco = case these (Symtab.lookup ((types_of o spec_of) thy) tyco)
  of (_, entry) :: _ => SOME entry
   | _ => NONE;
 
@@ -704,7 +706,7 @@
       (v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts;
     val inst = map2 (fn (v, sort) => fn (_, sort') =>
       (((v, 0), sort), Thm.global_ctyp_of thy (TFree (v, sort')))) vs mapping;
-    val subst = (map_types o map_type_tfree)
+    val subst = (Term.map_types o map_type_tfree)
       (fn (v, _) => TFree (v, the (AList.lookup (op =) mapping v)));
   in
     thm
@@ -783,15 +785,17 @@
         val cert_thm = Conjunction.intr_balanced (map rewrite_head thms');
       in Equations (cert_thm, propers) end;
 
-fun cert_of_proj thy c tyco =
+fun cert_of_proj ctxt c tyco =
   let
+    val thy = Proof_Context.theory_of ctxt
     val (vs, ((abs, (_, ty)), (rep, _))) = get_abstype_spec thy tyco;
     val _ = if c = rep then () else
       error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep);
   in Projection (mk_proj tyco vs ty abs rep, tyco) end;
 
-fun cert_of_abs thy tyco c raw_abs_thm =
+fun cert_of_abs ctxt tyco c raw_abs_thm =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val abs_thm = singleton (canonize_thms thy) raw_abs_thm;
     val _ = assert_abs_eqn thy (SOME tyco) abs_thm;
     val _ = if c = const_abs_eqn thy abs_thm then ()
@@ -906,9 +910,9 @@
 (* code certificate access with preprocessing *)
 
 fun retrieve_raw thy c =
-  Symtab.lookup ((the_functions o the_exec) thy) c
+  Symtab.lookup ((functions_of o spec_of) thy) c
   |> Option.map (snd o fst)
-  |> the_default None
+  |> the_default Unimplemented
 
 fun eqn_conv conv ct =
   let
@@ -939,30 +943,28 @@
   end;
 
 fun get_cert ctxt functrans c =
-  let
-    val thy = Proof_Context.theory_of ctxt;
-  in
-    case retrieve_raw thy c of
-      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
-    | None => nothing_cert ctxt c
-    | Proj ((_, tyco), _) => cert_of_proj thy c tyco
-    | Abstr ((abs_thm, tyco), _) => abs_thm
-       |> preprocess Conv.arg_conv ctxt
-       |> cert_of_abs thy tyco c
-  end;
+  case retrieve_raw (Proof_Context.theory_of ctxt) c of
+    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
+  | Proj ((_, tyco), _) => cert_of_proj ctxt c tyco
+  | Abstr ((abs_thm, tyco), _) => abs_thm
+     |> preprocess Conv.arg_conv ctxt
+     |> cert_of_abs ctxt tyco c;
 
 
-(* cases *)
+(* case certificates *)
 
-fun case_certificate thm =
+local
+
+fun raw_case_cert thm =
   let
     val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals
       o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.plain_prop_of) thm;
-    val _ = case head of Free _ => true
-      | Var _ => true
+    val _ = case head of Free _ => ()
+      | Var _ => ()
       | _ => raise TERM ("case_cert", []);
     val ([(case_var, _)], case_expr) = Term.strip_abs_eta 1 raw_case_expr;
     val (Const (case_const, _), raw_params) = strip_comb case_expr;
@@ -993,16 +995,20 @@
       | analyze cases = analyze_cases cases;
   in (case_const, (n, analyze cases)) end;
 
-fun case_cert thm = case_certificate thm
+in
+
+fun case_cert thm = raw_case_cert thm
   handle Bind => error "bad case certificate"
        | TERM _ => error "bad case certificate";
 
+end;
+
 fun get_case_scheme thy =
-  Option.map fst o (Symtab.lookup o the_cases o the_exec) thy;
+  Option.map fst o (Symtab.lookup o cases_of o spec_of) thy;
 fun get_case_cong thy =
-  Option.map snd o (Symtab.lookup o the_cases o the_exec) thy;
+  Option.map snd o (Symtab.lookup o cases_of o spec_of) thy;
 
-val undefineds = Symtab.keys o the_undefineds o the_exec;
+val undefineds = Symtab.keys o undefineds_of o spec_of;
 
 
 (* diagnostic *)
@@ -1010,14 +1016,14 @@
 fun print_codesetup thy =
   let
     val ctxt = Proof_Context.init_global thy;
-    val exec = the_exec thy;
+    val spec = spec_of thy;
     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)) =
           pretty_equations const (map fst (Lazy.force eqns_lazy))
-      | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
-      | pretty_function (const, None) = 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];
@@ -1042,17 +1048,18 @@
       | pretty_case (const, ((_, (_, cos)), _)) = (Pretty.block o Pretty.breaks) [
           Pretty.str (string_of_const thy const), Pretty.str "with",
           (Pretty.block o Pretty.commas o map (Pretty.str o pretty_caseparam)) cos];
-    val functions = the_functions exec
+    val functions = functions_of spec
       |> Symtab.dest
       |> (map o apsnd) (snd o fst)
+      |> filter (fn (_, Unimplemented) => false | _ => true)
       |> sort (string_ord o apply2 fst);
-    val datatypes = the_types exec
+    val datatypes = types_of spec
       |> Symtab.dest
       |> map (fn (tyco, (_, (vs, spec)) :: _) =>
           ((tyco, vs), constructors_of spec))
       |> sort (string_ord o apply2 (fst o fst));
-    val cases = Symtab.dest ((the_cases o the_exec) thy);
-    val undefineds = Symtab.keys ((the_undefineds o the_exec) thy);
+    val cases = Symtab.dest ((cases_of o spec_of) thy);
+    val undefineds = Symtab.keys ((undefineds_of o spec_of) thy);
   in
     Pretty.writeln_chunks [
       Pretty.block (
@@ -1100,7 +1107,7 @@
     fun update_subsume verbose (thm, proper) eqns = 
       let
         val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
-          o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
+          o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
         val args = args_of thm;
         val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1);
         fun matches_args args' =
@@ -1118,9 +1125,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 None = 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)];
@@ -1179,11 +1186,11 @@
 fun generic_del_eqn strictness thm thy = case mk_eqn strictness thy (thm, true)
  of SOME (thm, _) =>
       let
-        fun del_eqn' (Eqns_Default _) = initial_fun_spec
+        fun del_eqn' (Eqns_Default _) = default_fun_spec
           | del_eqn' (Eqns eqns) =
               let
                 val eqns' = filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns
-              in if null eqns' then None else Eqns eqns' end
+              in if null eqns' then Unimplemented else Eqns eqns' end
           | del_eqn' spec = spec
       in change_fun_spec (const_eqn thy thm) del_eqn' thy end
   | NONE => thy;
@@ -1191,7 +1198,7 @@
 val del_eqn_silent = generic_del_eqn Silent;
 val del_eqn = generic_del_eqn Liberal;
 
-fun del_eqns c = change_fun_spec c (K None);
+fun del_eqns c = change_fun_spec c (K Unimplemented);
 
 fun del_exception c = change_fun_spec c (K (Eqns []));
 
@@ -1231,16 +1238,16 @@
            then insert (op =) case_const cases
            else cases)
       | register_for_constructors (x as Abstractor _) = x;
-    val register_type = (map_typs o Symtab.map)
+    val register_type = (map_types o Symtab.map)
       (K ((map o apsnd o apsnd) register_for_constructors));
   in
     thy
     |> `(fn thy => case_cong thy case_const entry)
-    |-> (fn cong => map_exec_purge (register_case cong #> register_type))
+    |-> (fn cong => map_spec_purge (register_case cong #> register_type))
   end;
 
 fun add_undefined c thy =
-  (map_exec_purge o map_undefineds) (Symtab.update (c, ())) thy;
+  (map_spec_purge o map_undefineds) (Symtab.update (c, ())) thy;
 
 
 (* types *)
@@ -1248,7 +1255,7 @@
 fun register_type (tyco, vs_spec) thy =
   let
     val (old_constrs, some_old_proj) =
-      case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
+      case these (Symtab.lookup ((types_of o spec_of) thy) tyco)
        of (_, (_, Constructors (cos, _))) :: _ => (map fst cos, NONE)
         | (_, (_, Abstractor ((co, _), (proj, _)))) :: _ => ([co], SOME proj)
         | [] => ([], NONE);
@@ -1259,7 +1266,7 @@
           (fn (c, ((_, spec), _)) =>
             if member (op =) (the_list (associated_abstype spec)) tyco
             then insert (op =) c else I)
-            ((the_functions o the_exec) thy) [old_proj];
+            ((functions_of o spec_of) thy) [old_proj];
     fun drop_outdated_cases cases = fold Symtab.delete_safe
       (Symtab.fold (fn (c, ((_, (_, cos)), _)) =>
         if exists (member (op =) old_constrs) (map_filter I cos)
@@ -1267,8 +1274,8 @@
   in
     thy
     |> fold del_eqns (outdated_funs1 @ outdated_funs2)
-    |> map_exec_purge
-        ((map_typs o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec))
+    |> map_spec_purge
+        ((map_types o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec))
         #> map_cases drop_outdated_cases)
   end;