src/Pure/theory.ML
changeset 29581 b3b33e0298eb
parent 29092 466a83cb6f5f
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/theory.ML	Wed Jan 21 16:47:31 2009 +0100
     1.2 +++ b/src/Pure/theory.ML	Wed Jan 21 16:47:32 2009 +0100
     1.3 @@ -29,14 +29,14 @@
     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 add_axioms_i: (binding * term) list -> theory -> theory
     1.8    val add_axioms: (bstring * string) list -> theory -> theory
     1.9 -  val add_axioms_i: (bstring * term) list -> theory -> theory
    1.10    val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
    1.11 +  val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
    1.12    val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory
    1.13 -  val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
    1.14 +  val add_finals_i: bool -> term list -> theory -> theory
    1.15    val add_finals: bool -> string list -> theory -> theory
    1.16 -  val add_finals_i: bool -> term list -> theory -> theory
    1.17 -  val specify_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
    1.18 +  val specify_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
    1.19  end
    1.20  
    1.21  structure Theory: THEORY =
    1.22 @@ -157,19 +157,19 @@
    1.23  fun err_in_axm msg name =
    1.24    cat_error msg ("The error(s) above occurred in axiom " ^ quote name);
    1.25  
    1.26 -fun cert_axm thy (name, raw_tm) =
    1.27 +fun cert_axm thy (b, raw_tm) =
    1.28    let
    1.29      val (t, T, _) = Sign.certify_prop thy raw_tm
    1.30        handle TYPE (msg, _, _) => error msg
    1.31          | TERM (msg, _) => error msg;
    1.32    in
    1.33      Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
    1.34 -    (name, Sign.no_vars (Syntax.pp_global thy) t)
    1.35 +    (b, Sign.no_vars (Syntax.pp_global thy) t)
    1.36    end;
    1.37  
    1.38 -fun read_axm thy (name, str) =
    1.39 -  cert_axm thy (name, Syntax.read_prop_global thy str)
    1.40 -    handle ERROR msg => err_in_axm msg name;
    1.41 +fun read_axm thy (bname, str) =
    1.42 +  cert_axm thy (Binding.name bname, Syntax.read_prop_global thy str)
    1.43 +    handle ERROR msg => err_in_axm msg bname;
    1.44  
    1.45  
    1.46  (* add_axioms(_i) *)
    1.47 @@ -178,15 +178,15 @@
    1.48  
    1.49  fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
    1.50    let
    1.51 -    val axms = map (apfst Binding.name o apsnd Logic.varify o prep_axm thy) raw_axms;
    1.52 +    val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
    1.53      val axioms' = fold (snd oo NameSpace.bind (Sign.naming_of thy)) axms axioms
    1.54        handle Symtab.DUP dup => err_dup_axm dup;
    1.55    in axioms' end);
    1.56  
    1.57  in
    1.58  
    1.59 +val add_axioms_i = gen_add_axioms cert_axm;
    1.60  val add_axioms = gen_add_axioms read_axm;
    1.61 -val add_axioms_i = gen_add_axioms cert_axm;
    1.62  
    1.63  end;
    1.64  
    1.65 @@ -250,16 +250,16 @@
    1.66  
    1.67  (* check_def *)
    1.68  
    1.69 -fun check_def thy unchecked overloaded (bname, tm) defs =
    1.70 +fun check_def thy unchecked overloaded (b, tm) defs =
    1.71    let
    1.72      val ctxt = ProofContext.init thy;
    1.73 -    val name = Sign.full_bname thy bname;
    1.74 +    val name = Sign.full_name thy b;
    1.75      val (lhs_const, rhs) = Sign.cert_def ctxt tm;
    1.76      val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
    1.77      val _ = check_overloading thy overloaded lhs_const;
    1.78    in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
    1.79    handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    1.80 -   [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
    1.81 +   [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.display b) ^ ":"),
    1.82      Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
    1.83  
    1.84  
    1.85 @@ -298,8 +298,8 @@
    1.86  
    1.87  in
    1.88  
    1.89 +val add_finals_i = gen_add_finals (K I);
    1.90  val add_finals = gen_add_finals Syntax.read_term_global;
    1.91 -val add_finals_i = gen_add_finals (K I);
    1.92  
    1.93  end;
    1.94