--- 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);