merged
authorAndreas Lochbihler
Wed Oct 10 13:04:15 2012 +0200 (2012-10-10)
changeset 49771b1493798d253
parent 49770 cf6a78acf445
parent 49769 c7c2152322f2
child 49805 9a2a53be24a2
child 49807 9a0843995fd3
merged
     1.1 --- a/src/HOL/Finite_Set.thy	Wed Oct 10 13:03:50 2012 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Oct 10 13:04:15 2012 +0200
     1.3 @@ -16,18 +16,7 @@
     1.4      emptyI [simp, intro!]: "finite {}"
     1.5    | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
     1.6  
     1.7 -(* FIXME: move to Set theory *)
     1.8 -ML_file "Tools/set_comprehension_pointfree.ML"
     1.9 -
    1.10 -simproc_setup finite_Collect ("finite (Collect P)") =
    1.11 -  {* K Set_Comprehension_Pointfree.simproc *}
    1.12 -
    1.13 -(* FIXME: move to Set theory*)
    1.14 -setup {*
    1.15 -  Code_Preproc.map_pre (fn ss => ss addsimprocs
    1.16 -    [Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}],
    1.17 -    proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}])
    1.18 -*}
    1.19 +simproc_setup finite_Collect ("finite (Collect P)") = {* K Set_Comprehension_Pointfree.simproc *}
    1.20  
    1.21  lemma finite_induct [case_names empty insert, induct set: finite]:
    1.22    -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
     2.1 --- a/src/HOL/IMP/Collecting_Examples.thy	Wed Oct 10 13:03:50 2012 +0200
     2.2 +++ b/src/HOL/IMP/Collecting_Examples.thy	Wed Oct 10 13:04:15 2012 +0200
     2.3 @@ -7,12 +7,6 @@
     2.4  lemma insert_code [code]:  "insert x (set xs) = set (x#xs)"
     2.5  by simp
     2.6  
     2.7 -text{* Make assignment rule executable: *}
     2.8 -declare step.simps(2)[code del]
     2.9 -lemma [code]: "step S (x ::= e {P}) = (x ::= e {(%s. s(x := aval e s)) ` S})"
    2.10 -by auto
    2.11 -declare step.simps(1,3-)[code]
    2.12 -
    2.13  text{* The example: *}
    2.14  definition "c = WHILE Less (V ''x'') (N 3)
    2.15                  DO ''x'' ::= Plus (V ''x'') (N 2)"
     3.1 --- a/src/HOL/Lattices.thy	Wed Oct 10 13:03:50 2012 +0200
     3.2 +++ b/src/HOL/Lattices.thy	Wed Oct 10 13:04:15 2012 +0200
     3.3 @@ -650,14 +650,14 @@
     3.4  definition
     3.5    "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
     3.6  
     3.7 -lemma inf_apply [simp] (* CANDIDATE [code] *):
     3.8 +lemma inf_apply [simp, code]:
     3.9    "(f \<sqinter> g) x = f x \<sqinter> g x"
    3.10    by (simp add: inf_fun_def)
    3.11  
    3.12  definition
    3.13    "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
    3.14  
    3.15 -lemma sup_apply [simp] (* CANDIDATE [code] *):
    3.16 +lemma sup_apply [simp, code]:
    3.17    "(f \<squnion> g) x = f x \<squnion> g x"
    3.18    by (simp add: sup_fun_def)
    3.19  
    3.20 @@ -677,7 +677,7 @@
    3.21  definition
    3.22    fun_Compl_def: "- A = (\<lambda>x. - A x)"
    3.23  
    3.24 -lemma uminus_apply [simp] (* CANDIDATE [code] *):
    3.25 +lemma uminus_apply [simp, code]:
    3.26    "(- A) x = - (A x)"
    3.27    by (simp add: fun_Compl_def)
    3.28  
    3.29 @@ -691,7 +691,7 @@
    3.30  definition
    3.31    fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
    3.32  
    3.33 -lemma minus_apply [simp] (* CANDIDATE [code] *):
    3.34 +lemma minus_apply [simp, code]:
    3.35    "(A - B) x = A x - B x"
    3.36    by (simp add: fun_diff_def)
    3.37  
     4.1 --- a/src/HOL/Orderings.thy	Wed Oct 10 13:03:50 2012 +0200
     4.2 +++ b/src/HOL/Orderings.thy	Wed Oct 10 13:04:15 2012 +0200
     4.3 @@ -1296,7 +1296,7 @@
     4.4  definition
     4.5    "\<bottom> = (\<lambda>x. \<bottom>)"
     4.6  
     4.7 -lemma bot_apply [simp] (* CANDIDATE [code] *):
     4.8 +lemma bot_apply [simp, code]:
     4.9    "\<bottom> x = \<bottom>"
    4.10    by (simp add: bot_fun_def)
    4.11  
    4.12 @@ -1311,7 +1311,7 @@
    4.13  definition
    4.14    [no_atp]: "\<top> = (\<lambda>x. \<top>)"
    4.15  
    4.16 -lemma top_apply [simp] (* CANDIDATE [code] *):
    4.17 +lemma top_apply [simp, code]:
    4.18    "\<top> x = \<top>"
    4.19    by (simp add: top_fun_def)
    4.20  
     5.1 --- a/src/HOL/Product_Type.thy	Wed Oct 10 13:03:50 2012 +0200
     5.2 +++ b/src/HOL/Product_Type.thy	Wed Oct 10 13:04:15 2012 +0200
     5.3 @@ -1117,6 +1117,17 @@
     5.4  qed
     5.5  
     5.6  
     5.7 +subsection {* Simproc for rewriting a set comprehension into a pointfree expression *}
     5.8 +
     5.9 +ML_file "Tools/set_comprehension_pointfree.ML"
    5.10 +
    5.11 +setup {*
    5.12 +  Code_Preproc.map_pre (fn ss => ss addsimprocs
    5.13 +    [Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}],
    5.14 +    proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}])
    5.15 +*}
    5.16 +
    5.17 +
    5.18  subsection {* Inductively defined sets *}
    5.19  
    5.20  ML_file "Tools/inductive_set.ML"
     6.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 10 13:03:50 2012 +0200
     6.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 10 13:04:15 2012 +0200
     6.3 @@ -26,6 +26,20 @@
     6.4      Const (@{const_name Lattices.inf_class.inf}, T --> T --> T) $ t1 $ t2
     6.5    end
     6.6  
     6.7 +fun mk_sup (t1, t2) =
     6.8 +  let
     6.9 +    val T = fastype_of t1
    6.10 +  in
    6.11 +    Const (@{const_name Lattices.sup_class.sup}, T --> T --> T) $ t1 $ t2
    6.12 +  end
    6.13 +
    6.14 +fun mk_Compl t =
    6.15 +  let
    6.16 +    val T = fastype_of t
    6.17 +  in
    6.18 +    Const (@{const_name "Groups.uminus_class.uminus"}, T --> T) $ t
    6.19 +  end
    6.20 +
    6.21  fun mk_image t1 t2 =
    6.22    let
    6.23      val T as Type (@{type_name fun}, [_ , R]) = fastype_of t1
    6.24 @@ -68,11 +82,13 @@
    6.25  fun mk_pointfree_expr t =
    6.26    let
    6.27      val (vs, t'') = strip_ex (dest_Collect t)
    6.28 -    val (eq::conjs) = HOLogic.dest_conj t''
    6.29 -    val f = if fst (HOLogic.dest_eq eq) = Bound (length vs)
    6.30 -            then snd (HOLogic.dest_eq eq)
    6.31 -            else raise TERM("mk_pointfree_expr", [t]);
    6.32 -    val mems = map (apfst dest_Bound o HOLogic.dest_mem) conjs
    6.33 +    val conjs = HOLogic.dest_conj t''
    6.34 +    val is_the_eq =
    6.35 +      the_default false o (try (fn eq => fst (HOLogic.dest_eq eq) = Bound (length vs)))
    6.36 +    val SOME eq = find_first is_the_eq conjs
    6.37 +    val f = snd (HOLogic.dest_eq eq)
    6.38 +    val conjs' = filter_out (fn t => eq = t) conjs
    6.39 +    val mems = map (apfst dest_Bound o HOLogic.dest_mem) conjs'
    6.40      val grouped_mems = AList.group (op =) mems
    6.41      fun mk_grouped_unions (i, T) =
    6.42        case AList.lookup (op =) grouped_mems i of
    6.43 @@ -107,9 +123,8 @@
    6.44  
    6.45  val intro_Collect_tac = rtac @{thm iffD2[OF mem_Collect_eq]}
    6.46    THEN' REPEAT_DETERM1 o resolve_tac @{thms exI}
    6.47 -  THEN' (TRY o (rtac @{thm conjI}))
    6.48 -  THEN' (TRY o hyp_subst_tac)
    6.49 -  THEN' rtac @{thm refl};
    6.50 +  THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI}))
    6.51 +  THEN' (K (ALLGOALS (TRY o ((TRY o hyp_subst_tac) THEN' rtac @{thm refl}))))
    6.52  
    6.53  val tac =
    6.54    let
    6.55 @@ -125,20 +140,22 @@
    6.56      val subset_tac2 = rtac @{thm subsetI}
    6.57        THEN' dest_image_Sigma_tac
    6.58        THEN' intro_Collect_tac
    6.59 -      THEN' REPEAT_DETERM o
    6.60 -        (rtac @{thm conjI}
    6.61 -        ORELSE' eresolve_tac @{thms IntD1 IntD2}
    6.62 -        ORELSE' atac);
    6.63 +      THEN' REPEAT_DETERM o (eresolve_tac @{thms IntD1 IntD2} ORELSE' atac);
    6.64    in
    6.65      rtac @{thm subset_antisym} THEN' subset_tac1 THEN' subset_tac2
    6.66    end;
    6.67  
    6.68  fun conv ctxt t =
    6.69    let
    6.70 -    fun mk_thm t' = Goal.prove ctxt [] []
    6.71 -      (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) (K (tac 1));
    6.72 +    val ct = cterm_of (Proof_Context.theory_of ctxt) t
    6.73 +    val Bex_def = mk_meta_eq @{thm Bex_def}
    6.74 +    val unfold_eq = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv Bex_def))) ctxt ct
    6.75 +    val t' = term_of (Thm.rhs_of unfold_eq) 
    6.76 +    fun mk_thm t'' = Goal.prove ctxt [] []
    6.77 +      (HOLogic.mk_Trueprop (HOLogic.mk_eq (t', t''))) (K (tac 1))
    6.78 +    fun unfold th = th RS ((unfold_eq RS meta_eq_to_obj_eq) RS @{thm trans})
    6.79    in
    6.80 -    Option.map mk_thm (rewrite_term t)
    6.81 +    Option.map (unfold o mk_thm) (rewrite_term t')
    6.82    end;
    6.83  
    6.84  (* simproc *)
    6.85 @@ -152,15 +169,23 @@
    6.86      |> Option.map (fn thm => thm RS @{thm eq_reflection})
    6.87    end;
    6.88  
    6.89 -(* FIXME: turn into generic simproc for many predicates, i.e., remove hard-coded finite! *)
    6.90 +fun instantiate_arg_cong ctxt pred =
    6.91 +  let
    6.92 +    val certify = cterm_of (Proof_Context.theory_of ctxt)
    6.93 +    val arg_cong = @{thm arg_cong}
    6.94 +    val f $ _ = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (concl_of arg_cong)))
    6.95 +  in
    6.96 +    cterm_instantiate [(certify f, certify pred)] arg_cong
    6.97 +  end;
    6.98 +
    6.99  fun simproc ss redex =
   6.100    let
   6.101      val ctxt = Simplifier.the_context ss
   6.102 -    val _ $ set_compr = term_of redex
   6.103 +    val pred $ set_compr = term_of redex
   6.104 +    val arg_cong' = instantiate_arg_cong ctxt pred
   6.105    in
   6.106      conv ctxt set_compr
   6.107 -    |> Option.map (fn thm =>
   6.108 -         thm RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection})
   6.109 +    |> Option.map (fn thm => thm RS arg_cong' RS @{thm eq_reflection})
   6.110    end;
   6.111  
   6.112  fun code_simproc ss redex =
     7.1 --- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Wed Oct 10 13:03:50 2012 +0200
     7.2 +++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Wed Oct 10 13:04:15 2012 +0200
     7.3 @@ -59,6 +59,10 @@
     7.4    \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
     7.5    by simp
     7.6  
     7.7 +lemma
     7.8 +  "finite S ==> finite {s'. EX s:S. s' = f a e s}"
     7.9 +  by simp
    7.10 +
    7.11  schematic_lemma (* check interaction with schematics *)
    7.12    "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
    7.13     = finite ((\<lambda>(a:: ?'A, b :: ?'B). Pair_Rep a b) ` (UNIV \<times> UNIV))"
     8.1 --- a/src/Pure/Isar/code.ML	Wed Oct 10 13:03:50 2012 +0200
     8.2 +++ b/src/Pure/Isar/code.ML	Wed Oct 10 13:04:15 2012 +0200
     8.3 @@ -437,9 +437,14 @@
     8.4  
     8.5  exception BAD_THM of string;
     8.6  fun bad_thm msg = raise BAD_THM msg;
     8.7 -fun error_thm f thm = f thm handle BAD_THM msg => error msg;
     8.8 -fun warning_thm f thm = SOME (f thm) handle BAD_THM msg => (warning msg; NONE)
     8.9 -fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
    8.10 +fun error_thm f thy (thm, proper) = f (thm, proper)
    8.11 +  handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm);
    8.12 +fun error_abs_thm f thy thm = f thm
    8.13 +  handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm);
    8.14 +fun warning_thm f thy (thm, proper) = SOME (f (thm, proper))
    8.15 +  handle BAD_THM msg => (warning (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm); NONE)
    8.16 +fun try_thm f thm_proper = SOME (f thm_proper)
    8.17 +  handle BAD_THM _ => NONE;
    8.18  
    8.19  fun is_linear thm =
    8.20    let val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm
    8.21 @@ -458,30 +463,29 @@
    8.22  
    8.23  fun check_eqn thy { allow_nonlinear, allow_consts, allow_pats } thm (lhs, rhs) =
    8.24    let
    8.25 -    fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
    8.26      fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
    8.27 -      | Free _ => bad "Illegal free variable in equation"
    8.28 +      | Free _ => bad_thm "Illegal free variable"
    8.29        | _ => I) t [];
    8.30      fun tvars_of t = fold_term_types (fn _ =>
    8.31        fold_atyps (fn TVar (v, _) => insert (op =) v
    8.32 -        | TFree _ => bad "Illegal free type variable in equation")) t [];
    8.33 +        | TFree _ => bad_thm "Illegal free type variable")) t [];
    8.34      val lhs_vs = vars_of lhs;
    8.35      val rhs_vs = vars_of rhs;
    8.36      val lhs_tvs = tvars_of lhs;
    8.37      val rhs_tvs = tvars_of rhs;
    8.38      val _ = if null (subtract (op =) lhs_vs rhs_vs)
    8.39        then ()
    8.40 -      else bad "Free variables on right hand side of equation";
    8.41 +      else bad_thm "Free variables on right hand side of equation";
    8.42      val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
    8.43        then ()
    8.44 -      else bad "Free type variables on right hand side of equation";
    8.45 +      else bad_thm "Free type variables on right hand side of equation";
    8.46      val (head, args) = strip_comb lhs;
    8.47      val (c, ty) = case head
    8.48       of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty)
    8.49 -      | _ => bad "Equation not headed by constant";
    8.50 -    fun check _ (Abs _) = bad "Abstraction on left hand side of equation"
    8.51 +      | _ => bad_thm "Equation not headed by constant";
    8.52 +    fun check _ (Abs _) = bad_thm "Abstraction on left hand side of equation"
    8.53        | check 0 (Var _) = ()
    8.54 -      | check _ (Var _) = bad "Variable with application on left hand side of equation"
    8.55 +      | check _ (Var _) = bad_thm "Variable with application on left hand side of equation"
    8.56        | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
    8.57        | check n (Const (c_ty as (c, ty))) =
    8.58            if allow_pats then let
    8.59 @@ -489,70 +493,68 @@
    8.60            in if n = (length o binder_types) ty
    8.61              then if allow_consts orelse is_constr thy c'
    8.62                then ()
    8.63 -              else bad (quote c ^ " is not a constructor, on left hand side of equation")
    8.64 -            else bad ("Partially applied constant " ^ quote c ^ " on left hand side of equation")
    8.65 -          end else bad ("Pattern not allowed here, but constant " ^ quote c ^ " encountered on left hand side")
    8.66 +              else bad_thm (quote c ^ " is not a constructor, on left hand side of equation")
    8.67 +            else bad_thm ("Partially applied constant " ^ quote c ^ " on left hand side of equation")
    8.68 +          end else bad_thm ("Pattern not allowed here, but constant " ^ quote c ^ " encountered on left hand side of equation")
    8.69      val _ = map (check 0) args;
    8.70      val _ = if allow_nonlinear orelse is_linear thm then ()
    8.71 -      else bad "Duplicate variables on left hand side of equation";
    8.72 +      else bad_thm "Duplicate variables on left hand side of equation";
    8.73      val _ = if (is_none o AxClass.class_of_param thy) c then ()
    8.74 -      else bad "Overloaded constant as head in equation";
    8.75 +      else bad_thm "Overloaded constant as head in equation";
    8.76      val _ = if not (is_constr thy c) then ()
    8.77 -      else bad "Constructor as head in equation";
    8.78 +      else bad_thm "Constructor as head in equation";
    8.79      val _ = if not (is_abstr thy c) then ()
    8.80 -      else bad "Abstractor as head in equation";
    8.81 +      else bad_thm "Abstractor as head in equation";
    8.82      val _ = check_decl_ty thy (c, ty);
    8.83    in () end;
    8.84  
    8.85  fun gen_assert_eqn thy check_patterns (thm, proper) =
    8.86    let
    8.87 -    fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
    8.88      val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
    8.89 -      handle TERM _ => bad "Not an equation"
    8.90 -           | THM _ => bad "Not a proper equation";
    8.91 +      handle TERM _ => bad_thm "Not an equation"
    8.92 +           | THM _ => bad_thm "Not a proper equation";
    8.93      val _ = check_eqn thy { allow_nonlinear = not proper,
    8.94        allow_consts = not (proper andalso check_patterns), allow_pats = true } thm (lhs, rhs);
    8.95    in (thm, proper) end;
    8.96  
    8.97  fun assert_abs_eqn thy some_tyco thm =
    8.98    let
    8.99 -    fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
   8.100      val (full_lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
   8.101 -      handle TERM _ => bad "Not an equation"
   8.102 -           | THM _ => bad "Not a proper equation";
   8.103 +      handle TERM _ => bad_thm "Not an equation"
   8.104 +           | THM _ => bad_thm "Not a proper equation";
   8.105      val (rep, lhs) = dest_comb full_lhs
   8.106 -      handle TERM _ => bad "Not an abstract equation";
   8.107 +      handle TERM _ => bad_thm "Not an abstract equation";
   8.108      val (rep_const, ty) = dest_Const rep
   8.109 -      handle TERM _ => bad "Not an abstract equation";
   8.110 +      handle TERM _ => bad_thm "Not an abstract equation";
   8.111      val (tyco, Ts) = (dest_Type o domain_type) ty
   8.112 -      handle TERM _ => bad "Not an abstract equation"
   8.113 -           | TYPE _ => bad "Not an abstract equation";
   8.114 +      handle TERM _ => bad_thm "Not an abstract equation"
   8.115 +           | TYPE _ => bad_thm "Not an abstract equation";
   8.116      val _ = case some_tyco of SOME tyco' => if tyco = tyco' then ()
   8.117 -          else bad ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco')
   8.118 +          else bad_thm ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco')
   8.119        | NONE => ();
   8.120      val (vs', (_, (rep', _))) = get_abstype_spec thy tyco;
   8.121      val _ = if rep_const = rep' then ()
   8.122 -      else bad ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep');
   8.123 +      else bad_thm ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep');
   8.124      val _ = check_eqn thy { allow_nonlinear = false,
   8.125        allow_consts = false, allow_pats = false } thm (lhs, rhs);
   8.126      val _ = if forall2 (fn T => fn (_, sort) => Sign.of_sort thy (T, sort)) Ts vs' then ()
   8.127        else error ("Type arguments do not satisfy sort constraints of abstype certificate.");
   8.128    in (thm, tyco) end;
   8.129  
   8.130 -fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
   8.131 +fun assert_eqn thy = error_thm (gen_assert_eqn thy true) thy;
   8.132  
   8.133  fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy);
   8.134  
   8.135 -fun mk_eqn thy = error_thm (gen_assert_eqn thy false) o
   8.136 +fun mk_eqn thy = error_thm (gen_assert_eqn thy false) thy o
   8.137    apfst (meta_rewrite thy);
   8.138  
   8.139  fun mk_eqn_warning thy = Option.map (fn (thm, _) => (thm, is_linear thm))
   8.140 -  o warning_thm (gen_assert_eqn thy false) o rpair false o meta_rewrite thy;
   8.141 +  o warning_thm (gen_assert_eqn thy false) thy o rpair false o meta_rewrite thy;
   8.142  
   8.143  fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm))
   8.144    o try_thm (gen_assert_eqn thy false) o rpair false o meta_rewrite thy;
   8.145  
   8.146 -fun mk_abs_eqn thy = error_thm (assert_abs_eqn thy NONE) o meta_rewrite thy;
   8.147 +fun mk_abs_eqn thy = error_abs_thm (assert_abs_eqn thy NONE) thy o meta_rewrite thy;
   8.148  
   8.149  val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
   8.150  
   8.151 @@ -632,23 +634,22 @@
   8.152  fun check_abstype_cert thy proto_thm =
   8.153    let
   8.154      val thm = (AxClass.unoverload thy o meta_rewrite thy) proto_thm;
   8.155 -    fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
   8.156      val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm)
   8.157 -      handle TERM _ => bad "Not an equation"
   8.158 -           | THM _ => bad "Not a proper equation";
   8.159 +      handle TERM _ => bad_thm "Not an equation"
   8.160 +           | THM _ => bad_thm "Not a proper equation";
   8.161      val ((abs, raw_ty), ((rep, rep_ty), param)) = (apsnd (apfst dest_Const o dest_comb)
   8.162          o apfst dest_Const o dest_comb) lhs
   8.163 -      handle TERM _ => bad "Not an abstype certificate";
   8.164 +      handle TERM _ => bad_thm "Not an abstype certificate";
   8.165      val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
   8.166        then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
   8.167      val _ = check_decl_ty thy (abs, raw_ty);
   8.168      val _ = check_decl_ty thy (rep, rep_ty);
   8.169      val _ = if length (binder_types raw_ty) = 1
   8.170        then ()
   8.171 -      else bad "Bad type for abstract constructor";
   8.172 +      else bad_thm "Bad type for abstract constructor";
   8.173      val _ = (fst o dest_Var) param
   8.174 -      handle TERM _ => bad "Not an abstype certificate";
   8.175 -    val _ = if param = rhs then () else bad "Not an abstype certificate";
   8.176 +      handle TERM _ => bad_thm "Not an abstype certificate";
   8.177 +    val _ = if param = rhs then () else bad_thm "Not an abstype certificate";
   8.178      val ((tyco, sorts), (abs, (vs, ty'))) =
   8.179        analyze_constructor thy (abs, Logic.unvarifyT_global raw_ty);
   8.180      val ty = domain_type ty';
   8.181 @@ -1198,7 +1199,7 @@
   8.182  fun add_abstype proto_thm thy =
   8.183    let
   8.184      val (tyco, (vs, (abs_ty as (abs, (_, ty)), (rep, cert)))) =
   8.185 -      error_thm (check_abstype_cert thy) proto_thm;
   8.186 +      error_abs_thm (check_abstype_cert thy) thy proto_thm;
   8.187    in
   8.188      thy
   8.189      |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))