Syntax.parse/check/read;
authorwenzelm
Tue Sep 25 13:28:41 2007 +0200 (2007-09-25)
changeset 24708d9b00117365e
parent 24707 dfeb98f84e93
child 24709 ecfb9dcb6c4c
Syntax.parse/check/read;
no export of read/cert_axm;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Tue Sep 25 13:28:37 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Tue Sep 25 13:28:41 2007 +0200
     1.3 @@ -37,8 +37,6 @@
     1.4    val at_end: (theory -> theory option) -> theory -> theory
     1.5    val begin_theory: string -> theory list -> theory
     1.6    val end_theory: theory -> theory
     1.7 -  val cert_axm: theory -> string * term -> string * term
     1.8 -  val read_axm: theory -> string * string -> string * term
     1.9    val add_axioms: (bstring * string) list -> theory -> theory
    1.10    val add_axioms_i: (bstring * term) list -> theory -> theory
    1.11    val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
    1.12 @@ -215,7 +213,7 @@
    1.13    end;
    1.14  
    1.15  fun read_axm thy (name, str) =
    1.16 -  cert_axm thy (name, Sign.read_prop thy str)
    1.17 +  cert_axm thy (name, Syntax.read_prop_global thy str)
    1.18      handle ERROR msg => err_in_axm msg name;
    1.19  
    1.20  
    1.21 @@ -336,13 +334,14 @@
    1.22        | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
    1.23        | const_of _ = error "Attempt to finalize non-constant term";
    1.24      fun specify (c, T) = dependencies thy false false (c ^ " axiom") (c, T) [];
    1.25 -    val finalize = specify o check_overloading thy overloaded o const_of o prep_term thy;
    1.26 +    val finalize = specify o check_overloading thy overloaded o const_of o
    1.27 +      Sign.cert_term thy o prep_term thy;
    1.28    in thy |> map_defs (fold finalize args) end;
    1.29  
    1.30  in
    1.31  
    1.32 -val add_finals = gen_add_finals Sign.read_term;
    1.33 -val add_finals_i = gen_add_finals Sign.cert_term;
    1.34 +val add_finals = gen_add_finals Syntax.read_term_global;
    1.35 +val add_finals_i = gen_add_finals (K I);
    1.36  
    1.37  end;
    1.38