src/ZF/ind_syntax.ML

--- a/src/ZF/ind_syntax.ML	Mon Jan 29 14:16:13 1996 +0100
+++ b/src/ZF/ind_syntax.ML	Tue Jan 30 13:42:57 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	ZF/ind-syntax.ML
+(*  Title:      ZF/ind-syntax.ML
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Abstract Syntax functions for Inductive Definitions
@@ -53,22 +53,22 @@
 
 (*simple error-checking in the premises of an inductive definition*)
 fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
-	error"Premises may not be conjuctive"
+        error"Premises may not be conjuctive"
   | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
-	deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol"
+        deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol"
   | chk_prem rec_hd t = 
-	deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
+        deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
 
 (*Return the conclusion of a rule, of the form t:X*)
 fun rule_concl rl = 
     let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
-		Logic.strip_imp_concl rl
+                Logic.strip_imp_concl rl
     in  (t,X)  end;
 
 (*As above, but return error message if bad*)
 fun rule_concl_msg sign rl = rule_concl rl
     handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ 
-			  Sign.string_of_term sign rl);
+                          Sign.string_of_term sign rl);
 
 (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
   read_instantiate replaces a propositional variable by a formula variable*)
@@ -85,10 +85,10 @@
 (*read a constructor specification*)
 fun read_construct sign (id, sprems, syn) =
     let val prems = map (readtm sign oT) sprems
-	val args = map (#1 o dest_mem) prems
-	val T = (map (#2 o dest_Free) args) ---> iT
-		handle TERM _ => error 
-		    "Bad variable in constructor specification"
+        val args = map (#1 o dest_mem) prems
+        val T = (map (#2 o dest_Free) args) ---> iT
+                handle TERM _ => error 
+                    "Bad variable in constructor specification"
         val name = Syntax.const_name id syn  (*handle infix constructors*)
     in ((id,T,syn), name, args, prems) end;
 
@@ -97,17 +97,17 @@
 (*convert constructor specifications into introduction rules*)
 fun mk_intr_tms (rec_tm, constructs) =
   let fun mk_intr ((id,T,syn), name, args, prems) =
-	  Logic.list_implies
-	      (map mk_tprop prems,
-	       mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) 
+          Logic.list_implies
+              (map mk_tprop prems,
+               mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) 
   in  map mk_intr constructs  end;
 
 val mk_all_intr_tms = flat o map mk_intr_tms o op ~~;
 
-val Un		= Const("op Un", [iT,iT]--->iT)
-and empty	= Const("0", iT)
-and univ	= Const("univ", iT-->iT)
-and quniv	= Const("quniv", iT-->iT);
+val Un          = Const("op Un", [iT,iT]--->iT)
+and empty       = Const("0", iT)
+and univ        = Const("univ", iT-->iT)
+and quniv       = Const("quniv", iT-->iT);
 
 (*Make a datatype's domain: form the union of its set parameters*)
 fun union_params rec_tm =
@@ -135,9 +135,9 @@
 
 (*Includes rules for succ and Pair since they are common constructions*)
 val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
-		Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
-		make_elim succ_inject, 
-		refl_thin, conjE, exE, disjE];
+                Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
+                make_elim succ_inject, 
+                refl_thin, conjE, exE, disjE];
 
 (*Turns iff rules into safe elimination rules*)
 fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);