src/Pure/theory.ML
changeset 19693 ab816ca8df06
parent 19630 d370c3f5d3b2
child 19700 e02af528ceef
     1.1 --- a/src/Pure/theory.ML	Sat May 20 23:37:02 2006 +0200
     1.2 +++ b/src/Pure/theory.ML	Sat May 20 23:37:03 2006 +0200
     1.3 @@ -120,7 +120,7 @@
     1.4        val Thy {axioms = _, defs = defs2, oracles = oracles2} = thy2;
     1.5  
     1.6        val axioms = NameSpace.empty_table;
     1.7 -      val defs = Defs.merge (defs1, defs2);
     1.8 +      val defs = Defs.merge pp (defs1, defs2);
     1.9        val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
    1.10          handle Symtab.DUPS dups => err_dup_oras dups;
    1.11      in make_thy (axioms, defs, oracles) end;
    1.12 @@ -256,22 +256,17 @@
    1.13  
    1.14  fun check_def thy unchecked overloaded (bname, tm) defs =
    1.15    let
    1.16 -    val pp = Sign.pp thy;
    1.17 -    fun prt_const (c, T) =
    1.18 -     [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
    1.19 -      Pretty.quote (Pretty.typ pp (Type.freeze_type T))];
    1.20 -
    1.21      val name = Sign.full_name thy bname;
    1.22 -    val (lhs_const, rhs) = Sign.cert_def pp tm;
    1.23 +    val (lhs_const, rhs) = Sign.cert_def (Sign.pp thy) tm;
    1.24      val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
    1.25      val _ = check_overloading thy overloaded lhs_const;
    1.26    in
    1.27 -    defs |> Defs.define (Sign.const_typargs thy) unchecked true (Context.theory_name thy)
    1.28 +    defs |> Defs.define (Sign.pp thy) (Sign.consts_of thy) unchecked true (Context.theory_name thy)
    1.29        name (prep_const thy lhs_const) (map (prep_const thy) rhs_consts)
    1.30    end
    1.31    handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    1.32     [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
    1.33 -    Pretty.fbrk, Pretty.quote (Pretty.term (Sign.pp thy) tm)]));
    1.34 +    Pretty.fbrk, Pretty.quote (Sign.pretty_term thy tm)]));
    1.35  
    1.36  
    1.37  (* add_defs(_i) *)
    1.38 @@ -302,8 +297,8 @@
    1.39      fun const_of (Const const) = const
    1.40        | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
    1.41        | const_of _ = error "Attempt to finalize non-constant term";
    1.42 -    fun specify (c, T) = Defs.define (Sign.const_typargs thy) false false (Context.theory_name thy)
    1.43 -      (c ^ " axiom") (prep_const thy (c, T)) [];
    1.44 +    fun specify (c, T) = Defs.define (Sign.pp thy) (Sign.consts_of thy) false false
    1.45 +      (Context.theory_name thy) (c ^ " axiom") (prep_const thy (c, T)) [];
    1.46      val finalize = specify o check_overloading thy overloaded o
    1.47        const_of o Sign.no_vars (Sign.pp thy) o prep_term thy;
    1.48    in thy |> map_defs (fold finalize args) end;