# HG changeset patch # User wenzelm # Date 1190719721 -7200 # Node ID d9b00117365e02e88c28a335a9c1fcc2ba297e7f # Parent dfeb98f84e93bf4dba325cca20e15b322796a213 Syntax.parse/check/read; no export of read/cert_axm; diff -r dfeb98f84e93 -r d9b00117365e src/Pure/theory.ML --- a/src/Pure/theory.ML Tue Sep 25 13:28:37 2007 +0200 +++ b/src/Pure/theory.ML Tue Sep 25 13:28:41 2007 +0200 @@ -37,8 +37,6 @@ val at_end: (theory -> theory option) -> theory -> theory val begin_theory: string -> theory list -> theory val end_theory: theory -> theory - val cert_axm: theory -> string * term -> string * term - val read_axm: theory -> string * string -> string * term val add_axioms: (bstring * string) list -> theory -> theory val add_axioms_i: (bstring * term) list -> theory -> theory val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory @@ -215,7 +213,7 @@ end; fun read_axm thy (name, str) = - cert_axm thy (name, Sign.read_prop thy str) + cert_axm thy (name, Syntax.read_prop_global thy str) handle ERROR msg => err_in_axm msg name; @@ -336,13 +334,14 @@ | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)" | const_of _ = error "Attempt to finalize non-constant term"; fun specify (c, T) = dependencies thy false false (c ^ " axiom") (c, T) []; - val finalize = specify o check_overloading thy overloaded o const_of o prep_term thy; + val finalize = specify o check_overloading thy overloaded o const_of o + Sign.cert_term thy o prep_term thy; in thy |> map_defs (fold finalize args) end; in -val add_finals = gen_add_finals Sign.read_term; -val add_finals_i = gen_add_finals Sign.cert_term; +val add_finals = gen_add_finals Syntax.read_term_global; +val add_finals_i = gen_add_finals (K I); end;