src/Pure/term.ML
changeset 46217 7b19666f0e3d
parent 46215 0da9433f959e
child 46218 ecf6375e2abb
     1.1 --- a/src/Pure/term.ML	Sat Jan 14 18:18:06 2012 +0100
     1.2 +++ b/src/Pure/term.ML	Sat Jan 14 19:06:05 2012 +0100
     1.3 @@ -121,7 +121,6 @@
     1.4    val aT: sort -> typ
     1.5    val itselfT: typ -> typ
     1.6    val a_itselfT: typ
     1.7 -  val all: typ -> term
     1.8    val argument_type_of: term -> int -> typ
     1.9    val add_tvar_namesT: typ -> indexname list -> indexname list
    1.10    val add_tvar_names: term -> indexname list -> indexname list
    1.11 @@ -579,9 +578,7 @@
    1.12  fun itselfT ty = Type ("itself", [ty]);
    1.13  val a_itselfT = itselfT (TFree (Name.aT, []));
    1.14  
    1.15 -val propT : typ = Type("prop",[]);
    1.16 -
    1.17 -fun all T = Const("all", (T-->propT)-->propT);
    1.18 +val propT : typ = Type ("prop",[]);
    1.19  
    1.20  (* maps  !!x1...xn. t   to   t  *)
    1.21  fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
    1.22 @@ -766,7 +763,7 @@
    1.23  (*Quantification over a list of variables (already bound in body) *)
    1.24  fun list_all ([], t) = t
    1.25    | list_all ((a,T)::vars, t) =
    1.26 -        all T $ Abs (a, T, list_all (vars, t));
    1.27 +      Const ("all", (T --> propT) --> propT) $ Abs (a, T, list_all (vars, t));
    1.28  
    1.29  (*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
    1.30    A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)