# HG changeset patch
# User wenzelm
# Date 1269699631 -3600
# Node ID 0bbf0d2348f9e026363ec5cd9be0f5a1ca06fc65
# Parent  87e6e2737aee1ec600a6b930bd4810832157ee49
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def;
modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;

diff -r 87e6e2737aee -r 0bbf0d2348f9 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat Mar 27 14:10:37 2010 +0100
+++ b/src/Pure/Proof/extraction.ML	Sat Mar 27 15:20:31 2010 +0100
@@ -733,7 +733,7 @@
              thy'
              |> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
                   Thm.varifyT_global (funpow (length (OldTerm.term_vars corr_prop))
-                    (Thm.forall_elim_var 0) (forall_intr_frees
+                    (Thm.forall_elim_var 0) (Thm.forall_intr_frees
                       (ProofChecker.thm_of_proof thy'
                        (fst (Proofterm.freeze_thaw_prf prf))))))
              |> snd
diff -r 87e6e2737aee -r 0bbf0d2348f9 src/Pure/Proof/proofchecker.ML
--- a/src/Pure/Proof/proofchecker.ML	Sat Mar 27 14:10:37 2010 +0100
+++ b/src/Pure/Proof/proofchecker.ML	Sat Mar 27 15:20:31 2010 +0100
@@ -40,7 +40,7 @@
         val ctye = map (pairself (Thm.ctyp_of thy))
           (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
       in
-        Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm'))
+        Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
       end;
 
     fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
diff -r 87e6e2737aee -r 0bbf0d2348f9 src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Sat Mar 27 14:10:37 2010 +0100
+++ b/src/Pure/conjunction.ML	Sat Mar 27 15:20:31 2010 +0100
@@ -137,7 +137,7 @@
 
 fun comp_rule th rule =
   Thm.adjust_maxidx_thm ~1 (th COMP
-    (rule |> Drule.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
+    (rule |> Thm.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
 
 in
 
diff -r 87e6e2737aee -r 0bbf0d2348f9 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Mar 27 14:10:37 2010 +0100
+++ b/src/Pure/drule.ML	Sat Mar 27 15:20:31 2010 +0100
@@ -16,7 +16,6 @@
   val cterm_fun: (term -> term) -> (cterm -> cterm)
   val ctyp_fun: (typ -> typ) -> (ctyp -> ctyp)
   val forall_intr_list: cterm list -> thm -> thm
-  val forall_intr_frees: thm -> thm
   val forall_intr_vars: thm -> thm
   val forall_elim_list: cterm list -> thm -> thm
   val gen_all: thm -> thm
@@ -214,16 +213,6 @@
 (*Generalization over a list of variables*)
 val forall_intr_list = fold_rev forall_intr;
 
-(*Generalization over all suitable Free variables*)
-fun forall_intr_frees th =
-    let
-      val thy = Thm.theory_of_thm th;
-      val {prop, hyps, tpairs, ...} = rep_thm th;
-      val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) [];
-      val frees = Term.fold_aterms (fn Free v =>
-        if member (op =) fixed v then I else insert (op =) v | _ => I) prop [];
-    in fold (forall_intr o cterm_of thy o Free) frees th end;
-
 (*Generalization over Vars -- canonical order*)
 fun forall_intr_vars th =
   fold forall_intr
@@ -306,7 +295,7 @@
 
 val export_without_context_open =
   implies_intr_hyps
-  #> forall_intr_frees
+  #> Thm.forall_intr_frees
   #> `Thm.maxidx_of
   #-> (fn maxidx =>
     Thm.forall_elim_vars (maxidx + 1)
diff -r 87e6e2737aee -r 0bbf0d2348f9 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Mar 27 14:10:37 2010 +0100
+++ b/src/Pure/more_thm.ML	Sat Mar 27 15:20:31 2010 +0100
@@ -59,6 +59,7 @@
     (ctyp * ctyp) list * (cterm * cterm) list
   val certify_instantiate:
     ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
+  val forall_intr_frees: thm -> thm
   val unvarify_global: thm -> thm
   val close_derivation: thm -> thm
   val add_axiom: binding * term -> theory -> thm * theory
@@ -295,6 +296,18 @@
   Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th;
 
 
+(* forall_intr_frees: generalization over all suitable Free variables *)
+
+fun forall_intr_frees th =
+  let
+    val thy = Thm.theory_of_thm th;
+    val {prop, hyps, tpairs, ...} = Thm.rep_thm th;
+    val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) [];
+    val frees = Term.fold_aterms (fn Free v =>
+      if member (op =) fixed v then I else insert (op =) v | _ => I) prop [];
+  in fold (Thm.forall_intr o Thm.cterm_of thy o Free) frees th end;
+
+
 (* unvarify_global: global schematic variables *)
 
 fun unvarify_global th =
@@ -346,7 +359,7 @@
 fun add_def unchecked overloaded (b, prop) thy =
   let
     val (strip, recover, prop') = stripped_sorts thy prop;
-    val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy;
+    val thy' = Theory.add_def unchecked overloaded (b, prop') thy;
     val axm' = Thm.axiom thy' (Sign.full_name thy' b);
     val thm = unvarify_global (Thm.instantiate (recover, []) axm');
   in (thm, thy') end;
diff -r 87e6e2737aee -r 0bbf0d2348f9 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Mar 27 14:10:37 2010 +0100
+++ b/src/Pure/pure_thy.ML	Sat Mar 27 15:20:31 2010 +0100
@@ -200,16 +200,30 @@
 (* store axioms as theorems *)
 
 local
-  fun add_axm add = fold_map (fn ((b, prop), atts) => fn thy =>
-    let
-      val thy' = add [(b, prop)] thy;
-      val thm = Thm.forall_elim_vars 0 (Thm.axiom thy' (Sign.full_name thy' b));
-    in apfst hd (gen_add_thms (K I) [((b, thm), atts)] thy') end);
+
+fun no_read _ (_, t) = t;
+
+fun read thy (b, str) =
+  Syntax.read_prop_global thy str handle ERROR msg =>
+    cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b));
+
+fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
+  let
+    val prop = prep thy (b, raw_prop);
+    val (def, thy') = Thm.add_def unchecked overloaded (b, prop) thy;
+    val thm = def
+      |> Thm.forall_intr_frees
+      |> Thm.forall_elim_vars 0
+      |> Thm.varifyT_global;
+  in yield_singleton (gen_add_thms (K I)) ((b, thm), atts) thy' end);
+
 in
-  val add_defs               = add_axm o Theory.add_defs_i false;
-  val add_defs_unchecked     = add_axm o Theory.add_defs_i true;
-  val add_defs_cmd           = add_axm o Theory.add_defs false;
-  val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
+
+val add_defs = add no_read false;
+val add_defs_unchecked = add no_read true;
+val add_defs_cmd = add read false;
+val add_defs_unchecked_cmd = add read true;
+
 end;
 
 
diff -r 87e6e2737aee -r 0bbf0d2348f9 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Mar 27 14:10:37 2010 +0100
+++ b/src/Pure/theory.ML	Sat Mar 27 15:20:31 2010 +0100
@@ -30,8 +30,7 @@
   val end_theory: theory -> theory
   val add_axiom: binding * term -> theory -> theory
   val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
-  val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
-  val add_defs: bool -> bool -> (binding * string) list -> theory -> theory
+  val add_def: bool -> bool -> binding * term -> theory -> theory
   val add_finals_i: bool -> term list -> theory -> theory
   val add_finals: bool -> string list -> theory -> theory
   val specify_const: (binding * typ) * mixfix -> theory -> term * theory
@@ -151,9 +150,9 @@
 
 
 
-(** add axioms **)
+(** primitive specifications **)
 
-(* prepare axioms *)
+(* raw axioms *)
 
 fun cert_axm thy (b, raw_tm) =
   let
@@ -165,13 +164,6 @@
     (b, Sign.no_vars (Syntax.pp_global thy) t)
   end;
 
-fun read_axm thy (b, str) =
-  cert_axm thy (b, Syntax.read_prop_global thy str) handle ERROR msg =>
-    cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
-
-
-(* add_axiom *)
-
 fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms =>
   let
     val axm = apsnd Logic.varify_global (cert_axm thy raw_axm);
@@ -179,9 +171,6 @@
   in axioms' end);
 
 
-
-(** add constant definitions **)
-
 (* dependencies *)
 
 fun dependencies thy unchecked def description lhs rhs =
@@ -213,7 +202,7 @@
   in (t, add_deps "" const [] thy') end;
 
 
-(* check_overloading *)
+(* overloading *)
 
 fun check_overloading thy overloaded (c, T) =
   let
@@ -236,7 +225,9 @@
   end;
 
 
-(* check_def *)
+(* definitional axioms *)
+
+local
 
 fun check_def thy unchecked overloaded (b, tm) defs =
   let
@@ -250,22 +241,14 @@
    [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"),
     Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
 
-
-(* add_defs(_i) *)
-
-local
-
-fun gen_add_defs prep_axm unchecked overloaded raw_axms thy =
-  let val axms = map (prep_axm thy) raw_axms in
-    thy
-    |> map_defs (fold (check_def thy unchecked overloaded) axms)
-    |> fold add_axiom axms
-  end;
-
 in
 
-val add_defs_i = gen_add_defs cert_axm;
-val add_defs = gen_add_defs read_axm;
+fun add_def unchecked overloaded raw_axm thy =
+  let val axm = cert_axm thy raw_axm in
+    thy
+    |> map_defs (check_def thy unchecked overloaded axm)
+    |> add_axiom axm
+  end;
 
 end;