# HG changeset patch
# User wenzelm
# Date 1130531277 -7200
# Node ID 19f1ad18bece2e5775a7fa6fbd1116ca4b2fe604
# Parent  99a307bdfe15ddae225584b7878150699b01ed8c
renamed Goal constant to prop, more general protect/unprotect interfaces;
replaced lift_fns by lift_abs, lift_all;

diff -r 99a307bdfe15 -r 19f1ad18bece src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Oct 28 22:27:56 2005 +0200
+++ b/src/Pure/logic.ML	Fri Oct 28 22:27:57 2005 +0200
@@ -30,14 +30,15 @@
   val dest_type         : term -> typ
   val mk_inclass        : typ * class -> term
   val dest_inclass      : term -> typ * class
-  val goal_const        : term
-  val mk_goal           : term -> term
-  val dest_goal         : term -> term
+  val protectC          : term
+  val protect           : term -> term
+  val unprotect         : term -> term
   val occs              : term * term -> bool
   val close_form        : term -> term
   val incr_indexes      : typ list * int -> term -> term
   val incr_tvar         : int -> typ -> typ
-  val lift_fns          : term * int -> (term -> term) * (term -> term)
+  val lift_abs          : int -> term -> term -> term
+  val lift_all          : int -> term -> term -> term
   val strip_assums_hyp  : term -> term list
   val strip_assums_concl: term -> term
   val strip_params      : term -> (string * typ) list
@@ -165,13 +166,14 @@
   | dest_inclass t = raise TERM ("dest_inclass", [t]);
 
 
-(** atomic goals **)
+
+(** protected propositions **)
 
-val goal_const = Const ("Goal", propT --> propT);
-fun mk_goal t = goal_const $ t;
+val protectC = Const ("prop", propT --> propT);
+fun protect t = protectC $ t;
 
-fun dest_goal (Const ("Goal", _) $ t) = t
-  | dest_goal t = raise TERM ("dest_goal", [t]);
+fun unprotect (Const ("prop", _) $ t) = t
+  | unprotect t = raise TERM ("unprotect", [t]);
 
 
 (*** Low-level term operations ***)
@@ -203,13 +205,13 @@
 (*For all variables in the term, increment indexnames and lift over the Us
     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
 fun incr_indexes ([], 0) t = t
-  | incr_indexes (Us, k) t =
+  | incr_indexes (Ts, k) t =
   let
-    val n = length Us;
+    val n = length Ts;
     val incrT = if k = 0 then I else incrT k;
 
     fun incr lev (Var ((x, i), T)) =
-          Unify.combound (Var ((x, i + k), Us ---> (incrT T handle SAME => T)), lev, n)
+          Unify.combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
       | incr lev (Abs (x, T, body)) =
           (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
             handle SAME => Abs (x, T, incr (lev + 1) body))
@@ -228,19 +230,22 @@
 
 
 (*Make lifting functions from subgoal and increment.
-    lift_abs operates on tpairs (unification constraints)
-    lift_all operates on propositions     *)
-fun lift_fns (B,inc) =
-  let fun lift_abs (Us, Const("==>", _) $ _ $ B) u = lift_abs (Us,B) u
-        | lift_abs (Us, Const("all",_)$Abs(a,T,t)) u =
-              Abs(a, T, lift_abs (T::Us, t) u)
-        | lift_abs (Us, _) u = incr_indexes(rev Us, inc) u
-      fun lift_all (Us, Const("==>", _) $ A $ B) u =
-              implies $ A $ lift_all (Us,B) u
-        | lift_all (Us, Const("all",_)$Abs(a,T,t)) u =
-              all T $ Abs(a, T, lift_all (T::Us,t) u)
-        | lift_all (Us, _) u = incr_indexes(rev Us, inc) u;
-  in  (lift_abs([],B), lift_all([],B))  end;
+    lift_abs operates on terms
+    lift_all operates on propositions *)
+
+fun lift_abs inc =
+  let
+    fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
+      | lift Ts (Const ("all", _) $ Abs (a, T, b)) t = Abs (a, T, lift (T :: Ts) b t)
+      | lift Ts _ t = incr_indexes (rev Ts, inc) t;
+  in lift [] end;
+
+fun lift_all inc =
+  let
+    fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
+      | lift Ts ((c as Const ("all", _)) $ Abs (a, T, b)) t = c $ Abs (a, T, lift (T :: Ts) b t)
+      | lift Ts _ t = incr_indexes (rev Ts, inc) t;
+  in lift [] end;
 
 (*Strips assumptions in goal, yielding list of hypotheses.   *)
 fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B