src/Pure/theory.ML
changeset 35985 0bbf0d2348f9
parent 35857 28e73b3e7b6c
child 35987 7c728daf4876
     1.1 --- a/src/Pure/theory.ML	Sat Mar 27 14:10:37 2010 +0100
     1.2 +++ b/src/Pure/theory.ML	Sat Mar 27 15:20:31 2010 +0100
     1.3 @@ -30,8 +30,7 @@
     1.4    val end_theory: theory -> theory
     1.5    val add_axiom: binding * term -> theory -> theory
     1.6    val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
     1.7 -  val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
     1.8 -  val add_defs: bool -> bool -> (binding * string) list -> theory -> theory
     1.9 +  val add_def: bool -> bool -> binding * term -> theory -> theory
    1.10    val add_finals_i: bool -> term list -> theory -> theory
    1.11    val add_finals: bool -> string list -> theory -> theory
    1.12    val specify_const: (binding * typ) * mixfix -> theory -> term * theory
    1.13 @@ -151,9 +150,9 @@
    1.14  
    1.15  
    1.16  
    1.17 -(** add axioms **)
    1.18 +(** primitive specifications **)
    1.19  
    1.20 -(* prepare axioms *)
    1.21 +(* raw axioms *)
    1.22  
    1.23  fun cert_axm thy (b, raw_tm) =
    1.24    let
    1.25 @@ -165,13 +164,6 @@
    1.26      (b, Sign.no_vars (Syntax.pp_global thy) t)
    1.27    end;
    1.28  
    1.29 -fun read_axm thy (b, str) =
    1.30 -  cert_axm thy (b, Syntax.read_prop_global thy str) handle ERROR msg =>
    1.31 -    cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
    1.32 -
    1.33 -
    1.34 -(* add_axiom *)
    1.35 -
    1.36  fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms =>
    1.37    let
    1.38      val axm = apsnd Logic.varify_global (cert_axm thy raw_axm);
    1.39 @@ -179,9 +171,6 @@
    1.40    in axioms' end);
    1.41  
    1.42  
    1.43 -
    1.44 -(** add constant definitions **)
    1.45 -
    1.46  (* dependencies *)
    1.47  
    1.48  fun dependencies thy unchecked def description lhs rhs =
    1.49 @@ -213,7 +202,7 @@
    1.50    in (t, add_deps "" const [] thy') end;
    1.51  
    1.52  
    1.53 -(* check_overloading *)
    1.54 +(* overloading *)
    1.55  
    1.56  fun check_overloading thy overloaded (c, T) =
    1.57    let
    1.58 @@ -236,7 +225,9 @@
    1.59    end;
    1.60  
    1.61  
    1.62 -(* check_def *)
    1.63 +(* definitional axioms *)
    1.64 +
    1.65 +local
    1.66  
    1.67  fun check_def thy unchecked overloaded (b, tm) defs =
    1.68    let
    1.69 @@ -250,22 +241,14 @@
    1.70     [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"),
    1.71      Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
    1.72  
    1.73 -
    1.74 -(* add_defs(_i) *)
    1.75 -
    1.76 -local
    1.77 -
    1.78 -fun gen_add_defs prep_axm unchecked overloaded raw_axms thy =
    1.79 -  let val axms = map (prep_axm thy) raw_axms in
    1.80 -    thy
    1.81 -    |> map_defs (fold (check_def thy unchecked overloaded) axms)
    1.82 -    |> fold add_axiom axms
    1.83 -  end;
    1.84 -
    1.85  in
    1.86  
    1.87 -val add_defs_i = gen_add_defs cert_axm;
    1.88 -val add_defs = gen_add_defs read_axm;
    1.89 +fun add_def unchecked overloaded raw_axm thy =
    1.90 +  let val axm = cert_axm thy raw_axm in
    1.91 +    thy
    1.92 +    |> map_defs (check_def thy unchecked overloaded axm)
    1.93 +    |> add_axiom axm
    1.94 +  end;
    1.95  
    1.96  end;
    1.97