src/ZF/ind_syntax.ML

--- a/src/ZF/ind_syntax.ML	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/ZF/ind_syntax.ML	Sat Oct 17 14:43:18 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      ZF/ind_syntax.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
@@ -25,7 +24,7 @@
 fun mk_all_imp (A,P) =
     FOLogic.all_const iT $
       Abs("v", iT, FOLogic.imp $ (@{const mem} $ Bound 0 $ A) $
-	           Term.betapply(P, Bound 0));
+                   Term.betapply(P, Bound 0));
 
 fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT, t);
 
@@ -84,9 +83,9 @@
     fun mk_intr ((id,T,syn), name, args, prems) =
       Logic.list_implies
         (map FOLogic.mk_Trueprop prems,
-	 FOLogic.mk_Trueprop
-	    (@{const mem} $ list_comb (Const (Sign.full_bname sg name, T), args)
-	               $ rec_tm))
+         FOLogic.mk_Trueprop
+            (@{const mem} $ list_comb (Const (Sign.full_bname sg name, T), args)
+                       $ rec_tm))
   in  map mk_intr constructs  end;
 
 fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg);