# HG changeset patch
# User wenzelm
# Date 1082746251 -7200
# Node ID 148f6175fa783705b316a44ccad3a8235ff60127
# Parent  1d97b5f5526188b93f779c9018a708a14bed71d7
improved messages;

diff -r 1d97b5f55261 -r 148f6175fa78 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Fri Apr 23 20:50:16 2004 +0200
+++ b/src/Pure/Isar/constdefs.ML	Fri Apr 23 20:50:51 2004 +0200
@@ -25,9 +25,20 @@
 
 (** add_constdefs(_i) **)
 
+fun pretty_const sg (c, T) =
+  Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
+    Pretty.quote (Sign.pretty_typ sg T)];
+
+fun pretty_constdefs sg decls =
+  Pretty.big_list "constants" (map (pretty_const sg) decls);
+
 fun gen_constdef prep_typ prep_term prep_att
     structs (thy, (decl, ((raw_name, raw_atts), raw_prop))) =
   let
+    val sign = Theory.sign_of thy;
+    fun err msg ts =
+      error (cat_lines (msg :: map (Sign.string_of_term sign) ts));
+
     val ctxt =
       ProofContext.init thy |> ProofContext.add_fixes
         (flat (map (fn (As, T) => map (fn A => (A, T, None)) As) structs));
@@ -36,29 +47,33 @@
         (ProofContext.add_fixes [(x, apsome (prep_typ ctxt) raw_T, Some mx)] ctxt, mx));
 
     val prop = prep_term ctxt' raw_prop;
-    fun err msg = raise TERM (msg, [prop]);
+    val concl = Logic.strip_imp_concl prop;
+    val (lhs, _) = Logic.dest_equals concl handle TERM _ =>
+      err "Not a meta-equality (==):" [concl];
+    val head = Term.head_of lhs;
+    val (c, T) = Term.dest_Free head handle TERM _ =>
+      err "Locally fixed variable required as head of definition:" [head];
+    val _ = (case decl of None => () | Some (d, _, _) =>
+      if c <> d then
+        err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote d) []
+      else ());
 
-    val (lhs, _) = Logic.dest_equals (Logic.strip_imp_concl prop)
-      handle TERM _ => err "Not a meta-equality (==)";
-    val (c, T) = Term.dest_Free (Term.head_of lhs)
-      handle TERM _ => err "Head of definition needs to turn out as fixed variable";
-    val _ = (case decl of None => () | Some (d, _, _) =>
-      if c = d then ()
-      else err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote d));
-
-    val full = Sign.full_name (Theory.sign_of thy);
-    val def = Term.subst_atomic [(Free (c, T), Const (full c, T))] prop;
+    val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name sign c, T))] prop;
     val name = if raw_name = "" then Thm.def_name c else raw_name;
     val atts = map (prep_att thy) raw_atts;
-  in
-    thy
-    |> Theory.add_consts_i [(c, T, mx)]
-    |> PureThy.add_defs_i false [((name, def), atts)] |> #1
-  end;
+
+    val thy' =
+      thy
+      |> Theory.add_consts_i [(c, T, mx)]
+      |> PureThy.add_defs_i false [((name, def), atts)] |> #1;
+  in (thy', (c, T)) end;
 
 fun gen_constdefs prep_vars prep_typ prep_term prep_att (raw_structs, specs) thy =
-  let val structs = #2 (foldl_map prep_vars (ProofContext.init thy, raw_structs))
-  in foldl (gen_constdef prep_typ prep_term prep_att structs) (thy, specs) end;
+  let
+    val structs = #2 (foldl_map prep_vars (ProofContext.init thy, raw_structs));
+    val (thy', decls) = (thy, specs)
+      |> foldl_map (gen_constdef prep_typ prep_term prep_att structs);
+  in Pretty.writeln (pretty_constdefs (Theory.sign_of thy') decls); thy' end;
 
 val add_constdefs = gen_constdefs ProofContext.read_vars
   ProofContext.read_typ ProofContext.read_term Attrib.global_attribute;