1.1 --- a/src/Pure/Isar/constdefs.ML	Fri Apr 23 20:50:16 2004 +0200
     1.2 +++ b/src/Pure/Isar/constdefs.ML	Fri Apr 23 20:50:51 2004 +0200
     1.3 @@ -25,9 +25,20 @@
     1.4  
     1.5  (** add_constdefs(_i) **)
     1.6  
     1.7 +fun pretty_const sg (c, T) =
     1.8 +  Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
     1.9 +    Pretty.quote (Sign.pretty_typ sg T)];
    1.10 +
    1.11 +fun pretty_constdefs sg decls =
    1.12 +  Pretty.big_list "constants" (map (pretty_const sg) decls);
    1.13 +
    1.14  fun gen_constdef prep_typ prep_term prep_att
    1.15      structs (thy, (decl, ((raw_name, raw_atts), raw_prop))) =
    1.16    let
    1.17 +    val sign = Theory.sign_of thy;
    1.18 +    fun err msg ts =
    1.19 +      error (cat_lines (msg :: map (Sign.string_of_term sign) ts));
    1.20 +
    1.21      val ctxt =
    1.22        ProofContext.init thy |> ProofContext.add_fixes
    1.23          (flat (map (fn (As, T) => map (fn A => (A, T, None)) As) structs));
    1.24 @@ -36,29 +47,33 @@
    1.25          (ProofContext.add_fixes [(x, apsome (prep_typ ctxt) raw_T, Some mx)] ctxt, mx));
    1.26  
    1.27      val prop = prep_term ctxt' raw_prop;
    1.28 -    fun err msg = raise TERM (msg, [prop]);
    1.29 +    val concl = Logic.strip_imp_concl prop;
    1.30 +    val (lhs, _) = Logic.dest_equals concl handle TERM _ =>
    1.31 +      err "Not a meta-equality (==):" [concl];
    1.32 +    val head = Term.head_of lhs;
    1.33 +    val (c, T) = Term.dest_Free head handle TERM _ =>
    1.34 +      err "Locally fixed variable required as head of definition:" [head];
    1.35 +    val _ = (case decl of None => () | Some (d, _, _) =>
    1.36 +      if c <> d then
    1.37 +        err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote d) []
    1.38 +      else ());
    1.39  
    1.40 -    val (lhs, _) = Logic.dest_equals (Logic.strip_imp_concl prop)
    1.41 -      handle TERM _ => err "Not a meta-equality (==)";
    1.42 -    val (c, T) = Term.dest_Free (Term.head_of lhs)
    1.43 -      handle TERM _ => err "Head of definition needs to turn out as fixed variable";
    1.44 -    val _ = (case decl of None => () | Some (d, _, _) =>
    1.45 -      if c = d then ()
    1.46 -      else err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote d));
    1.47 -
    1.48 -    val full = Sign.full_name (Theory.sign_of thy);
    1.49 -    val def = Term.subst_atomic [(Free (c, T), Const (full c, T))] prop;
    1.50 +    val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name sign c, T))] prop;
    1.51      val name = if raw_name = "" then Thm.def_name c else raw_name;
    1.52      val atts = map (prep_att thy) raw_atts;
    1.53 -  in
    1.54 -    thy
    1.55 -    |> Theory.add_consts_i [(c, T, mx)]
    1.56 -    |> PureThy.add_defs_i false [((name, def), atts)] |> #1
    1.57 -  end;
    1.58 +
    1.59 +    val thy' =
    1.60 +      thy
    1.61 +      |> Theory.add_consts_i [(c, T, mx)]
    1.62 +      |> PureThy.add_defs_i false [((name, def), atts)] |> #1;
    1.63 +  in (thy', (c, T)) end;
    1.64  
    1.65  fun gen_constdefs prep_vars prep_typ prep_term prep_att (raw_structs, specs) thy =
    1.66 -  let val structs = #2 (foldl_map prep_vars (ProofContext.init thy, raw_structs))
    1.67 -  in foldl (gen_constdef prep_typ prep_term prep_att structs) (thy, specs) end;
    1.68 +  let
    1.69 +    val structs = #2 (foldl_map prep_vars (ProofContext.init thy, raw_structs));
    1.70 +    val (thy', decls) = (thy, specs)
    1.71 +      |> foldl_map (gen_constdef prep_typ prep_term prep_att structs);
    1.72 +  in Pretty.writeln (pretty_constdefs (Theory.sign_of thy') decls); thy' end;
    1.73  
    1.74  val add_constdefs = gen_constdefs ProofContext.read_vars
    1.75    ProofContext.read_typ ProofContext.read_term Attrib.global_attribute;