# HG changeset patch
# User wenzelm
# Date 1326564365 -3600
# Node ID 7b19666f0e3d253cec2207df6027be777f77a2ad
# Parent  7fcdb556246155f3ef6003653f797b97a3808012
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;

diff -r 7fcdb5562461 -r 7b19666f0e3d src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Sat Jan 14 18:18:06 2012 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Sat Jan 14 19:06:05 2012 +0100
@@ -115,7 +115,7 @@
           (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
             HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
         |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
-        |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
+        |> fold_rev (fn (n,T) => fn b => Logic.all_const T $ Abs(n,T,b)) (qs @ qs')
         |> curry abstract_over fvar
         |> curry subst_bound f
       end
@@ -389,7 +389,7 @@
     val thy = Proof_Context.theory_of ctxt
 
     (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
-    val ihyp = Term.all domT $ Abs ("z", domT,
+    val ihyp = Logic.all_const domT $ Abs ("z", domT,
       Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
         HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
           Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
@@ -600,7 +600,7 @@
       |> cterm_of thy
 
     (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
-    val ihyp = Term.all domT $ Abs ("z", domT,
+    val ihyp = Logic.all_const domT $ Abs ("z", domT,
       Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
         HOLogic.mk_Trueprop (P $ Bound 0)))
       |> cterm_of thy
@@ -780,7 +780,7 @@
       |> cterm_of thy (* "wf R'" *)
 
     (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
-    val ihyp = Term.all domT $ Abs ("z", domT,
+    val ihyp = Logic.all_const domT $ Abs ("z", domT,
       Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
         HOLogic.mk_Trueprop (acc_R $ Bound 0)))
       |> cterm_of thy
diff -r 7fcdb5562461 -r 7b19666f0e3d src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Sat Jan 14 18:18:06 2012 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Sat Jan 14 19:06:05 2012 +0100
@@ -217,7 +217,7 @@
     val P_comp = mk_ind_goal thy branches
 
     (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
-    val ihyp = Term.all T $ Abs ("z", T,
+    val ihyp = Logic.all_const T $ Abs ("z", T,
       Logic.mk_implies
         (HOLogic.mk_Trueprop (
           Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
diff -r 7fcdb5562461 -r 7b19666f0e3d src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 14 18:18:06 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 14 19:06:05 2012 +0100
@@ -894,7 +894,7 @@
   let
     fun close_up zs zs' =
       fold (fn (z as ((s, _), T)) => fn t' =>
-               Term.all T $ Abs (s, T, abstract_over (Var z, t')))
+               Logic.all_const T $ Abs (s, T, abstract_over (Var z, t')))
            (take (length zs' - length zs) zs')
     fun aux zs (@{const "==>"} $ t1 $ t2) =
         let val zs' = Term.add_vars t1 zs in
diff -r 7fcdb5562461 -r 7b19666f0e3d src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Jan 14 18:18:06 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Jan 14 19:06:05 2012 +0100
@@ -163,7 +163,7 @@
   |> fold (fn ((s, i), T) => fn (t', taken) =>
               let val s' = singleton (Name.variant_list taken) s in
                 ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
-                  else Term.all) T
+                  else Logic.all_const) T
                  $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
                  s' :: taken)
               end)
diff -r 7fcdb5562461 -r 7b19666f0e3d src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sat Jan 14 18:18:06 2012 +0100
+++ b/src/HOL/Tools/refute.ML	Sat Jan 14 19:06:05 2012 +0100
@@ -416,7 +416,7 @@
     val vars = sort_wrt (fst o fst) (Term.add_vars t [])
   in
     fold (fn ((x, i), T) => fn t' =>
-      Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
+      Logic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
   end;
 
 val monomorphic_term = ATP_Util.monomorphic_term
diff -r 7fcdb5562461 -r 7b19666f0e3d src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Jan 14 18:18:06 2012 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Jan 14 19:06:05 2012 +0100
@@ -102,7 +102,7 @@
       | abs_body _ _ a = a;
     fun close (y, U) B =
       let val B' = abs_body 0 y (Term.incr_boundvars 1 B)
-      in if Term.is_dependent B' then Term.all dummyT $ Abs (y, U, B') else B end;
+      in if Term.is_dependent B' then Logic.all_const dummyT $ Abs (y, U, B') else B end;
     fun close_form A =
       let
         val occ_frees = rev (Variable.add_free_names ctxt A []);
diff -r 7fcdb5562461 -r 7b19666f0e3d src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Sat Jan 14 18:18:06 2012 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Sat Jan 14 19:06:05 2012 +0100
@@ -305,7 +305,7 @@
 
 fun prop_of0 Hs (PBound i) = nth Hs i
   | prop_of0 Hs (Abst (s, SOME T, prf)) =
-      Term.all T $ (Abs (s, T, prop_of0 Hs prf))
+      Logic.all_const T $ (Abs (s, T, prop_of0 Hs prf))
   | prop_of0 Hs (AbsP (s, SOME t, prf)) =
       Logic.mk_implies (t, prop_of0 (t :: Hs) prf)
   | prop_of0 Hs (prf % SOME t) = (case head_norm (prop_of0 Hs prf) of
diff -r 7fcdb5562461 -r 7b19666f0e3d src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sat Jan 14 18:18:06 2012 +0100
+++ b/src/Pure/logic.ML	Sat Jan 14 19:06:05 2012 +0100
@@ -7,6 +7,7 @@
 
 signature LOGIC =
 sig
+  val all_const: typ -> term
   val all: term -> term -> term
   val is_all: term -> bool
   val dest_all: term -> (string * typ) * term
@@ -91,7 +92,9 @@
 
 (** all **)
 
-fun all v t = Const ("all", (Term.fastype_of v --> propT) --> propT) $ lambda v t;
+fun all_const T = Const ("all", (T --> propT) --> propT);
+
+fun all v t = all_const (Term.fastype_of v) $ lambda v t;
 
 fun is_all (Const ("all", _) $ Abs _) = true
   | is_all _ = false;
@@ -161,7 +164,7 @@
 
 (** conjunction **)
 
-val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
+val true_prop = all_const propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
 val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);
 
 
diff -r 7fcdb5562461 -r 7b19666f0e3d src/Pure/term.ML
--- a/src/Pure/term.ML	Sat Jan 14 18:18:06 2012 +0100
+++ b/src/Pure/term.ML	Sat Jan 14 19:06:05 2012 +0100
@@ -121,7 +121,6 @@
   val aT: sort -> typ
   val itselfT: typ -> typ
   val a_itselfT: typ
-  val all: typ -> term
   val argument_type_of: term -> int -> typ
   val add_tvar_namesT: typ -> indexname list -> indexname list
   val add_tvar_names: term -> indexname list -> indexname list
@@ -579,9 +578,7 @@
 fun itselfT ty = Type ("itself", [ty]);
 val a_itselfT = itselfT (TFree (Name.aT, []));
 
-val propT : typ = Type("prop",[]);
-
-fun all T = Const("all", (T-->propT)-->propT);
+val propT : typ = Type ("prop",[]);
 
 (* maps  !!x1...xn. t   to   t  *)
 fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
@@ -766,7 +763,7 @@
 (*Quantification over a list of variables (already bound in body) *)
 fun list_all ([], t) = t
   | list_all ((a,T)::vars, t) =
-        all T $ Abs (a, T, list_all (vars, t));
+      Const ("all", (T --> propT) --> propT) $ Abs (a, T, list_all (vars, t));
 
 (*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
diff -r 7fcdb5562461 -r 7b19666f0e3d src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Jan 14 18:18:06 2012 +0100
+++ b/src/Pure/thm.ML	Sat Jan 14 19:06:05 2012 +0100
@@ -753,7 +753,7 @@
         shyps = Sorts.union sorts shyps,
         hyps = hyps,
         tpairs = tpairs,
-        prop = Term.all T $ Abs (a, T, abstract_over (x, prop))});
+        prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))});
     fun check_occs a x ts =
       if exists (fn t => Logic.occs (x, t)) ts then
         raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th])
@@ -1588,7 +1588,7 @@
         val T' = Envir.subst_type (Envir.type_env env) T
         (*Must instantiate types of parameters because they are flattened;
           this could be a NEW parameter*)
-      in Term.all T' $ Abs (a, T', norm_term_skip env n t) end
+      in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end
   | norm_term_skip env n (Const ("==>", _) $ A $ B) =
       Logic.mk_implies (A, norm_term_skip env (n - 1) B)
   | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??";
diff -r 7fcdb5562461 -r 7b19666f0e3d src/Tools/IsaPlanner/isand.ML
--- a/src/Tools/IsaPlanner/isand.ML	Sat Jan 14 18:18:06 2012 +0100
+++ b/src/Tools/IsaPlanner/isand.ML	Sat Jan 14 19:06:05 2012 +0100
@@ -130,7 +130,7 @@
       val premts = Thm.prems_of th;
     
       fun allify_prem_var (vt as (n,ty),t)  = 
-          (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
+          (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
 
       fun allify_prem Ts p = List.foldr allify_prem_var p Ts
 
@@ -171,7 +171,7 @@
 fun assume_allified sgn (tyvs,vs) t = 
     let
       fun allify_var (vt as (n,ty),t)  = 
-          (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
+          (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
       fun allify Ts p = List.foldr allify_var p Ts
 
       val ctermify = Thm.cterm_of sgn;
@@ -303,7 +303,7 @@
 fun allify_term (v, t) = 
     let val vt = #t (Thm.rep_cterm v)
       val (n,ty) = Term.dest_Free vt
-    in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
+    in (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
 
 fun allify_for_sg_term ctermify vs t =
     let val t_alls = List.foldr allify_term t vs;