Removal of redundant code (unused or already present in Isabelle.
authorpaulson
Tue May 20 11:49:57 1997 +0200 (1997-05-20)
changeset 3245241838c01caf
parent 3244 71b760618f30
child 3246 7f783705c7a4
Removal of redundant code (unused or already present in Isabelle.
This eliminates HOL compatibility but makes the code smaller and more
readable
TFL/dcterm.sml
TFL/post.sml
TFL/rules.new.sml
TFL/rules.sig
TFL/sys.sml
TFL/tfl.sig
TFL/tfl.sml
TFL/thms.sig
TFL/thms.sml
TFL/thry.sig
TFL/thry.sml
TFL/usyntax.sig
TFL/usyntax.sml
TFL/utils.sig
TFL/utils.sml
     1.1 --- a/TFL/dcterm.sml	Tue May 20 11:47:33 1997 +0200
     1.2 +++ b/TFL/dcterm.sml	Tue May 20 11:49:57 1997 +0200
     1.3 @@ -4,9 +4,6 @@
     1.4  
     1.5  structure Dcterm :
     1.6  sig
     1.7 -    val caconv : cterm -> cterm -> bool
     1.8 -    val mk_eq : cterm * cterm -> cterm
     1.9 -    val mk_imp : cterm * cterm -> cterm
    1.10      val mk_conj : cterm * cterm -> cterm
    1.11      val mk_disj : cterm * cterm -> cterm
    1.12      val mk_select : cterm * cterm -> cterm
    1.13 @@ -40,12 +37,9 @@
    1.14      val is_pair : cterm -> bool
    1.15      val is_select : cterm -> bool
    1.16      val is_var : cterm -> bool
    1.17 -    val list_mk_comb : cterm * cterm list -> cterm
    1.18      val list_mk_abs : cterm list -> cterm -> cterm
    1.19 -    val list_mk_imp : cterm list * cterm -> cterm
    1.20      val list_mk_exists : cterm list * cterm -> cterm
    1.21      val list_mk_forall : cterm list * cterm -> cterm
    1.22 -    val list_mk_conj : cterm list -> cterm
    1.23      val list_mk_disj : cterm list -> cterm
    1.24      val strip_abs : cterm -> cterm list * cterm
    1.25      val strip_comb : cterm -> cterm * cterm list
    1.26 @@ -68,7 +62,6 @@
    1.27  val can = Utils.can;
    1.28  val quote = Utils.quote;
    1.29  fun swap (x,y) = (y,x);
    1.30 -val bool = Type("bool",[]);
    1.31  
    1.32  fun itlist f L base_value =
    1.33     let fun it [] = base_value
    1.34 @@ -76,24 +69,7 @@
    1.35     in it L 
    1.36     end;
    1.37  
    1.38 -fun end_itlist f =
    1.39 -let fun endit [] = raise ERR"end_itlist" "list too short"
    1.40 -      | endit alist = 
    1.41 -         let val (base::ralist) = rev alist
    1.42 -         in itlist f (rev ralist) base  end
    1.43 -in endit
    1.44 -end;
    1.45 -
    1.46 -fun rev_itlist f =
    1.47 -   let fun rev_it [] base = base
    1.48 -         | rev_it (a::rst) base = rev_it rst (f a base)
    1.49 -   in rev_it
    1.50 -   end;
    1.51 -
    1.52 -(*---------------------------------------------------------------------------
    1.53 - * Alpha conversion.
    1.54 - *---------------------------------------------------------------------------*)
    1.55 -fun caconv ctm1 ctm2 = Term.aconv(#t(rep_cterm ctm1),#t(rep_cterm ctm2));
    1.56 +val end_itlist = Utils.end_itlist;
    1.57  
    1.58  
    1.59  (*---------------------------------------------------------------------------
    1.60 @@ -103,44 +79,30 @@
    1.61  fun mk_const sign pr = cterm_of sign (Const pr);
    1.62  val mk_hol_const = mk_const (sign_of HOL.thy);
    1.63  
    1.64 -fun list_mk_comb (h,[]) = h
    1.65 -  | list_mk_comb (h,L) = rev_itlist (fn t1 => fn t2 => capply t2 t1) L h;
    1.66 -
    1.67 -
    1.68 -fun mk_eq(lhs,rhs) = 
    1.69 -   let val ty = #T(rep_cterm lhs)
    1.70 -       val c = mk_hol_const("op =", ty --> ty --> bool)
    1.71 -   in list_mk_comb(c,[lhs,rhs])
    1.72 -   end;
    1.73 -
    1.74 -local val c = mk_hol_const("op -->", bool --> bool --> bool)
    1.75 -in fun mk_imp(ant,conseq) = list_mk_comb(c,[ant,conseq])
    1.76 -end;
    1.77 -
    1.78  fun mk_select (r as (Bvar,Body)) = 
    1.79    let val ty = #T(rep_cterm Bvar)
    1.80 -      val c = mk_hol_const("Eps", (ty --> bool) --> ty)
    1.81 +      val c = mk_hol_const("Eps", (ty --> HOLogic.boolT) --> ty)
    1.82    in capply c (uncurry cabs r)
    1.83    end;
    1.84  
    1.85  fun mk_forall (r as (Bvar,Body)) = 
    1.86    let val ty = #T(rep_cterm Bvar)
    1.87 -      val c = mk_hol_const("All", (ty --> bool) --> bool)
    1.88 +      val c = mk_hol_const("All", (ty --> HOLogic.boolT) --> HOLogic.boolT)
    1.89    in capply c (uncurry cabs r)
    1.90    end;
    1.91  
    1.92  fun mk_exists (r as (Bvar,Body)) = 
    1.93    let val ty = #T(rep_cterm Bvar)
    1.94 -      val c = mk_hol_const("Ex", (ty --> bool) --> bool)
    1.95 +      val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT)
    1.96    in capply c (uncurry cabs r)
    1.97    end;
    1.98  
    1.99  
   1.100 -local val c = mk_hol_const("op &", bool --> bool --> bool)
   1.101 +local val c = mk_hol_const("op &", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   1.102  in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
   1.103  end;
   1.104  
   1.105 -local val c = mk_hol_const("op |", bool --> bool --> bool)
   1.106 +local val c = mk_hol_const("op |", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   1.107  in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
   1.108  end;
   1.109  
   1.110 @@ -226,10 +188,8 @@
   1.111   *---------------------------------------------------------------------------*)
   1.112  val list_mk_abs = itlist cabs;
   1.113  
   1.114 -fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp(a,tm)) A c;
   1.115  fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v, b)) V t;
   1.116  fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall(v, b)) V t;
   1.117 -val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj(c1, tm))
   1.118  val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1, tm))
   1.119  
   1.120  (*---------------------------------------------------------------------------
     2.1 --- a/TFL/post.sml	Tue May 20 11:47:33 1997 +0200
     2.2 +++ b/TFL/post.sml	Tue May 20 11:49:57 1997 +0200
     2.3 @@ -1,3 +1,11 @@
     2.4 +(*-------------------------------------------------------------------------
     2.5 +there are 3 postprocessors that get applied to the definition:
     2.6 +
     2.7 +    - a wellfoundedness prover (WF_TAC)
     2.8 +    - a simplifier (tries to eliminate the language of termination expressions)
     2.9 +    - a termination prover
    2.10 +*-------------------------------------------------------------------------*)
    2.11 +
    2.12  signature TFL = 
    2.13    sig
    2.14     structure Prim : TFL_sig
    2.15 @@ -38,7 +46,7 @@
    2.16   * have a tactic directly applied to them.
    2.17   *--------------------------------------------------------------------------*)
    2.18  fun termination_goals rules = 
    2.19 -    map (Logic.freeze_vars o S.drop_Trueprop)
    2.20 +    map (Logic.freeze_vars o HOLogic.dest_Trueprop)
    2.21        (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));
    2.22  
    2.23   (*---------------------------------------------------------------------------
    2.24 @@ -48,26 +56,23 @@
    2.25   fun tgoalw thy defs rules = 
    2.26      let val L = termination_goals rules
    2.27          open USyntax
    2.28 -        val g = cterm_of (sign_of thy) (mk_prop(list_mk_conj L))
    2.29 +        val g = cterm_of (sign_of thy) (HOLogic.mk_Trueprop(list_mk_conj L))
    2.30      in goalw_cterm defs g
    2.31      end;
    2.32  
    2.33 - val tgoal = Utils.C tgoalw [];
    2.34 + fun tgoal thy = tgoalw thy [];
    2.35  
    2.36   (*---------------------------------------------------------------------------
    2.37    * Simple wellfoundedness prover.
    2.38    *--------------------------------------------------------------------------*)
    2.39   fun WF_TAC thms = REPEAT(FIRST1(map rtac thms))
    2.40 - val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, wf_less_than,
    2.41 -                    wf_pred_nat, wf_pred_list, wf_trancl];
    2.42 + val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, wf_less_than, 
    2.43 +                    wf_pred_list, wf_trancl];
    2.44  
    2.45 - val terminator = simp_tac(!simpset addsimps [less_than_def, pred_nat_def,
    2.46 -					      pred_list_def]) 1
    2.47 + val terminator = simp_tac(!simpset addsimps [less_Suc_eq, pred_list_def]) 1
    2.48                    THEN TRY(best_tac
    2.49 -			   (!claset addSDs [not0_implies_Suc]
    2.50 -				    addIs [r_into_trancl,
    2.51 -					   trans_trancl RS transD]
    2.52 -				    addss (!simpset)) 1);
    2.53 +                           (!claset addSDs [not0_implies_Suc]
    2.54 +                                    addss (!simpset)) 1);
    2.55  
    2.56   val simpls = [less_eq RS eq_reflection,
    2.57                 lex_prod_def, rprod_def, measure_def, inv_image_def];
    2.58 @@ -83,7 +88,7 @@
    2.59                                      simplifier = Prim.Rules.simpl_conv simpls};
    2.60  
    2.61   val simplifier = rewrite_rule (simpls @ #simps(rep_ss (!simpset)) @ 
    2.62 -                                [less_than_def, pred_nat_def, pred_list_def]);
    2.63 +                                [pred_list_def]);
    2.64  
    2.65   fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
    2.66  
    2.67 @@ -102,12 +107,12 @@
    2.68    end;
    2.69  
    2.70  (*lcp's version: takes strings; doesn't return "thm" 
    2.71 -	(whose signature is a draft and therefore useless) *)
    2.72 +        (whose signature is a draft and therefore useless) *)
    2.73  fun define thy R eqs = 
    2.74    let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) 
    2.75        val (thy',(_,pats)) =
    2.76 -	     define_i thy (read thy R) 
    2.77 -	              (fold_bal (app Ind_Syntax.conj) (map (read thy) eqs))
    2.78 +             define_i thy (read thy R) 
    2.79 +                      (fold_bal (app Ind_Syntax.conj) (map (read thy) eqs))
    2.80    in  (thy',pats)  end
    2.81    handle Utils.ERR {mesg,...} => error mesg;
    2.82  
    2.83 @@ -134,7 +139,7 @@
    2.84       Const("==",_)$_$_ => r
    2.85    |   _$(Const("op =",_)$_$_) => r RS eq_reflection
    2.86    |   _ => r RS P_imp_P_eq_True
    2.87 -fun rewrite L = rewrite_rule (map mk_meta_eq (Utils.filter(not o id_thm) L))
    2.88 +fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L))
    2.89  fun reducer thl = rewrite (map standard thl @ #simps(rep_ss HOL_ss))
    2.90  
    2.91  fun join_assums th = 
    2.92 @@ -143,7 +148,7 @@
    2.93        val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
    2.94        val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
    2.95        val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
    2.96 -      val cntxt = U.union S.aconv cntxtl cntxtr
    2.97 +      val cntxt = gen_union (op aconv) (cntxtl, cntxtr)
    2.98    in 
    2.99      R.GEN_ALL 
   2.100        (R.DISCH_ALL 
   2.101 @@ -198,22 +203,22 @@
   2.102  fun simplify_defn (thy,(id,pats)) =
   2.103     let val dummy = deny (id  mem  map ! (stamps_of_thy thy))
   2.104                          ("Recursive definition " ^ id ^ 
   2.105 -			 " would clash with the theory of the same name!")
   2.106 +                         " would clash with the theory of the same name!")
   2.107         val def = freezeT(get_def thy id  RS  meta_eq_to_obj_eq)
   2.108         val {theory,rules,TCs,full_pats_TCs,patterns} = 
   2.109 -		Prim.post_definition (thy,(def,pats))
   2.110 +                Prim.post_definition (thy,(def,pats))
   2.111         val {lhs=f,rhs} = S.dest_eq(concl def)
   2.112         val (_,[R,_]) = S.strip_comb rhs
   2.113         val {induction, rules, tcs} = 
   2.114               proof_stage theory reducer
   2.115 -	       {f = f, R = R, rules = rules,
   2.116 -		full_pats_TCs = full_pats_TCs,
   2.117 -		TCs = TCs}
   2.118 +               {f = f, R = R, rules = rules,
   2.119 +                full_pats_TCs = full_pats_TCs,
   2.120 +                TCs = TCs}
   2.121         val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules)
   2.122     in  {induct = meta_outer
   2.123 -	          (normalize_thm [RSspec,RSmp] (induction RS spec')), 
   2.124 -	rules = rules', 
   2.125 -	tcs = (termination_goals rules') @ tcs}
   2.126 +                  (normalize_thm [RSspec,RSmp] (induction RS spec')), 
   2.127 +        rules = rules', 
   2.128 +        tcs = (termination_goals rules') @ tcs}
   2.129     end
   2.130    handle Utils.ERR {mesg,...} => error mesg
   2.131  end;
     3.1 --- a/TFL/rules.new.sml	Tue May 20 11:47:33 1997 +0200
     3.2 +++ b/TFL/rules.new.sml	Tue May 20 11:49:57 1997 +0200
     3.3 @@ -10,23 +10,16 @@
     3.4  structure U  = Utils;
     3.5  structure D = Dcterm;
     3.6  
     3.7 -type Type = USyntax.Type
     3.8 -type Preterm  = USyntax.Preterm
     3.9 -type Term = USyntax.Term
    3.10 -type Thm = Thm.thm
    3.11 -type Tactic = tactic;
    3.12  
    3.13  fun RULES_ERR{func,mesg} = Utils.ERR{module = "FastRules",func=func,mesg=mesg};
    3.14  
    3.15 -nonfix ##;    val ## = Utils.##;      infix  4 ##; 
    3.16  
    3.17  fun cconcl thm = D.drop_prop(#prop(crep_thm thm));
    3.18  fun chyps thm = map D.drop_prop(#hyps(crep_thm thm));
    3.19  
    3.20  fun dest_thm thm = 
    3.21 -   let val drop = S.drop_Trueprop
    3.22 -       val {prop,hyps,...} = rep_thm thm
    3.23 -   in (map drop hyps, drop prop)
    3.24 +   let val {prop,hyps,...} = rep_thm thm
    3.25 +   in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop)
    3.26     end;
    3.27  
    3.28  
    3.29 @@ -46,11 +39,9 @@
    3.30     in equal_elim (transitive ctm2_eq ctm1_eq) thm
    3.31     end;
    3.32  
    3.33 -val BETA_RULE = Utils.I;
    3.34 -
    3.35  
    3.36  (*----------------------------------------------------------------------------
    3.37 - *        Type instantiation
    3.38 + *        typ instantiation
    3.39   *---------------------------------------------------------------------------*)
    3.40  fun INST_TYPE blist thm = 
    3.41    let val {sign,...} = rep_thm thm
    3.42 @@ -82,9 +73,9 @@
    3.43  
    3.44  
    3.45  fun FILTER_DISCH_ALL P thm =
    3.46 - let fun check tm = U.holds P (S.drop_Trueprop (#t(rep_cterm tm)))
    3.47 - in  U.itlist (fn tm => fn th => if (check tm) then DISCH tm th else th)
    3.48 -              (chyps thm) thm
    3.49 + let fun check tm = U.holds P (#t(rep_cterm tm))
    3.50 + in  foldr (fn (tm,th) => if (check tm) then DISCH tm th else th)
    3.51 +              (chyps thm, thm)
    3.52   end;
    3.53  
    3.54  (* freezeT expensive! *)
    3.55 @@ -97,10 +88,10 @@
    3.56  fun PROVE_HYP ath bth =  MP (DISCH (cconcl ath) bth) ath;
    3.57  
    3.58  local val [p1,p2] = goal HOL.thy "(A-->B) ==> (B --> C) ==> (A-->C)"
    3.59 -      val _ = by (rtac impI 1)
    3.60 -      val _ = by (rtac (p2 RS mp) 1)
    3.61 -      val _ = by (rtac (p1 RS mp) 1)
    3.62 -      val _ = by (assume_tac 1)
    3.63 +      val dummy = by (rtac impI 1)
    3.64 +      val dummy = by (rtac (p2 RS mp) 1)
    3.65 +      val dummy = by (rtac (p1 RS mp) 1)
    3.66 +      val dummy = by (assume_tac 1)
    3.67        val imp_trans = result()
    3.68  in
    3.69  fun IMP_TRANS th1 th2 = th2 RS (th1 RS imp_trans)
    3.70 @@ -167,11 +158,11 @@
    3.71   *
    3.72   *---------------------------------------------------------------------------*)
    3.73  local val [p1,p2,p3] = goal HOL.thy "(P | Q) ==> (P --> R) ==> (Q --> R) ==> R"
    3.74 -      val _ = by (rtac (p1 RS disjE) 1)
    3.75 -      val _ = by (rtac (p2 RS mp) 1)
    3.76 -      val _ = by (assume_tac 1)
    3.77 -      val _ = by (rtac (p3 RS mp) 1)
    3.78 -      val _ = by (assume_tac 1)
    3.79 +      val dummy = by (rtac (p1 RS disjE) 1)
    3.80 +      val dummy = by (rtac (p2 RS mp) 1)
    3.81 +      val dummy = by (assume_tac 1)
    3.82 +      val dummy = by (rtac (p3 RS mp) 1)
    3.83 +      val dummy = by (assume_tac 1)
    3.84        val tfl_exE = result()
    3.85  in
    3.86  fun DISJ_CASES th1 th2 th3 = 
    3.87 @@ -215,7 +206,9 @@
    3.88  (* freezeT expensive! *)
    3.89  fun DISJ_CASESL disjth thl =
    3.90     let val c = cconcl disjth
    3.91 -       fun eq th atm = exists (D.caconv atm) (chyps th)
    3.92 +       fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t 
    3.93 +			               aconv term_of atm)
    3.94 +	                      (#hyps(rep_thm th))
    3.95         val tml = D.strip_disj c
    3.96         fun DL th [] = raise RULES_ERR{func="DISJ_CASESL",mesg="no cases"}
    3.97           | DL th [th1] = PROVE_HYP th th1
    3.98 @@ -262,7 +255,7 @@
    3.99  fun GEN v th =
   3.100     let val gth = forall_intr v th
   3.101         val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth
   3.102 -       val P' = Abs(x,ty, S.drop_Trueprop rst)  (* get rid of trueprop *)
   3.103 +       val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
   3.104         val tsig = #tsig(Sign.rep_sg sign)
   3.105         val theta = Pattern.match tsig (P,P')
   3.106         val allI2 = instantiate (certify sign theta) allI
   3.107 @@ -289,8 +282,8 @@
   3.108    let val fth = freezeT th
   3.109        val {prop,sign,...} = rep_thm fth
   3.110        fun mk_inst (Var(v,T)) = 
   3.111 -	  (cterm_of sign (Var(v,T)),
   3.112 -	   cterm_of sign (Free(string_of v, T)))
   3.113 +          (cterm_of sign (Var(v,T)),
   3.114 +           cterm_of sign (Free(string_of v, T)))
   3.115        val insts = map mk_inst (term_vars prop)
   3.116    in  instantiate ([],insts) fth  
   3.117    end
   3.118 @@ -318,10 +311,10 @@
   3.119   *---------------------------------------------------------------------------*)
   3.120  
   3.121  local val [p1,p2] = goal HOL.thy "(? x. P x) ==> (!x. P x --> Q) ==> Q"
   3.122 -      val _ = by (rtac (p1 RS exE) 1)
   3.123 -      val _ = by (rtac ((p2 RS allE) RS mp) 1)
   3.124 -      val _ = by (assume_tac 2)
   3.125 -      val _ = by (assume_tac 1)
   3.126 +      val dummy = by (rtac (p1 RS exE) 1)
   3.127 +      val dummy = by (rtac ((p2 RS allE) RS mp) 1)
   3.128 +      val dummy = by (assume_tac 2)
   3.129 +      val dummy = by (assume_tac 1)
   3.130        val choose_thm = result()
   3.131  in
   3.132  fun CHOOSE(fvar,exth) fact =
   3.133 @@ -378,7 +371,7 @@
   3.134         
   3.135    in
   3.136    U.itlist (fn (b as (r1 |-> r2)) => fn thm => 
   3.137 -        EXISTS(?r2(S.subst[b] (S.drop_Trueprop(#prop(rep_thm thm)))), tych r1)
   3.138 +        EXISTS(?r2(S.subst[b] (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
   3.139                thm)
   3.140         blist' th
   3.141    end;
   3.142 @@ -426,10 +419,6 @@
   3.143   *---------------------------------------------------------------------------*)
   3.144  
   3.145  
   3.146 -
   3.147 -val bool = S.bool
   3.148 -val prop = Type("prop",[]);
   3.149 -
   3.150  (* Object language quantifier, i.e., "!" *)
   3.151  fun Forall v M = S.mk_forall{Bvar=v, Body=M};
   3.152  
   3.153 @@ -452,8 +441,8 @@
   3.154    | dest_equal tm = S.dest_eq tm;
   3.155  
   3.156  
   3.157 -fun get_rhs tm = #rhs(dest_equal (S.drop_Trueprop tm));
   3.158 -fun get_lhs tm = #lhs(dest_equal (S.drop_Trueprop tm));
   3.159 +fun get_rhs tm = #rhs(dest_equal (HOLogic.dest_Trueprop tm));
   3.160 +fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
   3.161  
   3.162  fun variants FV vlist =
   3.163    rev(#1(U.rev_itlist (fn v => fn (V,W) =>
   3.164 @@ -589,17 +578,11 @@
   3.165  
   3.166  local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
   3.167        fun mk_fst tm = 
   3.168 -          let val ty = S.type_of tm
   3.169 -              val {Tyop="*",Args=[fty,sty]} = S.dest_type ty
   3.170 -              val fst = S.mk_const{Name="fst",Ty = ty --> fty}
   3.171 -          in S.mk_comb{Rator=fst, Rand=tm}
   3.172 -          end
   3.173 +          let val ty as Type("*", [fty,sty]) = type_of tm
   3.174 +          in  Const ("fst", ty --> fty) $ tm  end
   3.175        fun mk_snd tm = 
   3.176 -          let val ty = S.type_of tm
   3.177 -              val {Tyop="*",Args=[fty,sty]} = S.dest_type ty
   3.178 -              val snd = S.mk_const{Name="snd",Ty = ty --> sty}
   3.179 -          in S.mk_comb{Rator=snd, Rand=tm}
   3.180 -          end
   3.181 +          let val ty as Type("*", [fty,sty]) = type_of tm
   3.182 +          in  Const ("snd", ty --> sty) $ tm  end
   3.183  in
   3.184  fun XFILL tych x vstruct = 
   3.185    let fun traverse p xocc L =
   3.186 @@ -622,7 +605,7 @@
   3.187  
   3.188  fun VSTRUCT_ELIM tych a vstr th = 
   3.189    let val L = S.free_vars_lr vstr
   3.190 -      val bind1 = tych (S.mk_prop (S.mk_eq{lhs=a, rhs=vstr}))
   3.191 +      val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
   3.192        val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th)
   3.193        val thm2 = forall_intr_list (map tych L) thm1
   3.194        val thm3 = forall_elim_list (XFILL tych a vstr) thm2
   3.195 @@ -648,7 +631,7 @@
   3.196   *---------------------------------------------------------------------------*)
   3.197  fun dest_pbeta_redex M n = 
   3.198    let val (f,args) = dest_combn M n
   3.199 -      val _ = dest_aabs f
   3.200 +      val dummy = dest_aabs f
   3.201    in (strip_aabs f,args)
   3.202    end;
   3.203  
   3.204 @@ -666,30 +649,30 @@
   3.205  
   3.206  fun CONTEXT_REWRITE_RULE(func,R){thms=[cut_lemma],congs,th} =
   3.207   let val tc_list = ref[]: term list ref
   3.208 -     val _ = term_ref := []
   3.209 -     val _ = thm_ref  := []
   3.210 -     val _ = mss_ref  := []
   3.211 +     val dummy = term_ref := []
   3.212 +     val dummy = thm_ref  := []
   3.213 +     val dummy = mss_ref  := []
   3.214       val cut_lemma' = (cut_lemma RS mp) RS eq_reflection
   3.215       fun prover mss thm =
   3.216       let fun cong_prover mss thm =
   3.217 -         let val _ = say "cong_prover:\n"
   3.218 +         let val dummy = say "cong_prover:\n"
   3.219               val cntxt = prems_of_mss mss
   3.220 -             val _ = print_thms "cntxt:\n" cntxt
   3.221 -             val _ = say "cong rule:\n"
   3.222 -             val _ = say (string_of_thm thm^"\n")
   3.223 -             val _ = thm_ref := (thm :: !thm_ref)
   3.224 -             val _ = mss_ref := (mss :: !mss_ref)
   3.225 +             val dummy = print_thms "cntxt:\n" cntxt
   3.226 +             val dummy = say "cong rule:\n"
   3.227 +             val dummy = say (string_of_thm thm^"\n")
   3.228 +             val dummy = thm_ref := (thm :: !thm_ref)
   3.229 +             val dummy = mss_ref := (mss :: !mss_ref)
   3.230               (* Unquantified eliminate *)
   3.231               fun uq_eliminate (thm,imp,sign) = 
   3.232                   let val tych = cterm_of sign
   3.233 -                     val _ = print_cterms "To eliminate:\n" [tych imp]
   3.234 +                     val dummy = print_cterms "To eliminate:\n" [tych imp]
   3.235                       val ants = map tych (Logic.strip_imp_prems imp)
   3.236                       val eq = Logic.strip_imp_concl imp
   3.237                       val lhs = tych(get_lhs eq)
   3.238                       val mss' = add_prems(mss, map ASSUME ants)
   3.239                       val lhs_eq_lhs1 = rewrite_cterm(false,true)mss' prover lhs
   3.240                         handle _ => reflexive lhs
   3.241 -                     val _ = print_thms "proven:\n" [lhs_eq_lhs1]
   3.242 +                     val dummy = print_thms "proven:\n" [lhs_eq_lhs1]
   3.243                       val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
   3.244                       val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
   3.245                    in
   3.246 @@ -697,10 +680,12 @@
   3.247                    end
   3.248               fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) =
   3.249                let val ((vstrl,_),args) = dest_pbeta_redex lhs_eq(length vlist)
   3.250 -                  val true = forall (fn (tm1,tm2) => S.aconv tm1 tm2)
   3.251 -                                   (Utils.zip vlist args)
   3.252 +                  val dummy = assert (forall (op aconv)
   3.253 +                                      (ListPair.zip (vlist, args)))
   3.254 +                               "assertion failed in CONTEXT_REWRITE_RULE"
   3.255  (*                val fbvs1 = variants (S.free_vars imp) fbvs *)
   3.256 -                  val imp_body1 = S.subst (map (op|->) (U.zip args vstrl))
   3.257 +                  val imp_body1 = S.subst (map (op|->) 
   3.258 +                                           (ListPair.zip (args, vstrl)))
   3.259                                            imp_body
   3.260                    val tych = cterm_of sign
   3.261                    val ants1 = map tych (Logic.strip_imp_prems imp_body1)
   3.262 @@ -711,8 +696,8 @@
   3.263                    val mss' = add_prems(mss, map ASSUME ants1)
   3.264                    val Q1eeqQ2 = rewrite_cterm (false,true) mss' prover Q1
   3.265                                  handle _ => reflexive Q1
   3.266 -                  val Q2 = get_rhs(S.drop_Trueprop(#prop(rep_thm Q1eeqQ2)))
   3.267 -                  val Q3 = tych(S.list_mk_comb(list_mk_aabs(vstrl,Q2),vstrl))
   3.268 +                  val Q2 = get_rhs(HOLogic.dest_Trueprop(#prop(rep_thm Q1eeqQ2)))
   3.269 +                  val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
   3.270                    val Q2eeqQ3 = symmetric(pbeta_reduce Q3 RS eq_reflection)
   3.271                    val thA = transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
   3.272                    val QeeqQ3 = transitive thA Q2eeqQ3 handle _ =>
   3.273 @@ -757,12 +742,12 @@
   3.274           end handle _ => None
   3.275  
   3.276          fun restrict_prover mss thm =
   3.277 -          let val _ = say "restrict_prover:\n"
   3.278 +          let val dummy = say "restrict_prover:\n"
   3.279                val cntxt = rev(prems_of_mss mss)
   3.280 -              val _ = print_thms "cntxt:\n" cntxt
   3.281 +              val dummy = print_thms "cntxt:\n" cntxt
   3.282                val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
   3.283                     sign,...} = rep_thm thm
   3.284 -              fun genl tm = let val vlist = U.set_diff (U.curry(op aconv))
   3.285 +              fun genl tm = let val vlist = U.set_diff (curry(op aconv))
   3.286                                             (add_term_frees(tm,[])) [func,R]
   3.287                              in U.itlist Forall vlist tm
   3.288                              end
   3.289 @@ -780,19 +765,19 @@
   3.290                                 handle _ => false
   3.291                val nested = U.can(S.find_term is_func)
   3.292                val rcontext = rev cntxt
   3.293 -              val cncl = S.drop_Trueprop o #prop o rep_thm
   3.294 +              val cncl = HOLogic.dest_Trueprop o #prop o rep_thm
   3.295                val antl = case rcontext of [] => [] 
   3.296                           | _   => [S.list_mk_conj(map cncl rcontext)]
   3.297                val TC = genl(S.list_mk_imp(antl, A))
   3.298 -              val _ = print_cterms "func:\n" [cterm_of sign func]
   3.299 -              val _ = print_cterms "TC:\n" [cterm_of sign (S.mk_prop TC)]
   3.300 -              val _ = tc_list := (TC :: !tc_list)
   3.301 +              val dummy = print_cterms "func:\n" [cterm_of sign func]
   3.302 +              val dummy = print_cterms "TC:\n" [cterm_of sign (HOLogic.mk_Trueprop TC)]
   3.303 +              val dummy = tc_list := (TC :: !tc_list)
   3.304                val nestedp = nested TC
   3.305 -              val _ = if nestedp then say "nested\n" else say "not_nested\n"
   3.306 -              val _ = term_ref := ([func,TC]@(!term_ref))
   3.307 +              val dummy = if nestedp then say "nested\n" else say "not_nested\n"
   3.308 +              val dummy = term_ref := ([func,TC]@(!term_ref))
   3.309                val th' = if nestedp then raise RULES_ERR{func = "solver", 
   3.310                                                        mesg = "nested function"}
   3.311 -                        else let val cTC = cterm_of sign (S.mk_prop TC)
   3.312 +                        else let val cTC = cterm_of sign (HOLogic.mk_Trueprop TC)
   3.313                               in case rcontext of
   3.314                                  [] => SPEC_ALL(ASSUME cTC)
   3.315                                 | _ => MP (SPEC_ALL (ASSUME cTC)) 
   3.316 @@ -809,14 +794,14 @@
   3.317                              prover ctm
   3.318      val th2 = equal_elim th1 th
   3.319   in
   3.320 - (th2, U.filter (not o restricted) (!tc_list))
   3.321 + (th2, filter (not o restricted) (!tc_list))
   3.322   end;
   3.323  
   3.324  
   3.325  
   3.326  fun prove (tm,tac) = 
   3.327    let val {t,sign,...} = rep_cterm tm
   3.328 -      val ptm = cterm_of sign(S.mk_prop t)
   3.329 +      val ptm = cterm_of sign(HOLogic.mk_Trueprop t)
   3.330    in
   3.331    freeze(prove_goalw_cterm [] ptm (fn _ => [tac]))
   3.332    end;
     4.1 --- a/TFL/rules.sig	Tue May 20 11:47:33 1997 +0200
     4.2 +++ b/TFL/rules.sig	Tue May 20 11:49:57 1997 +0200
     4.3 @@ -1,65 +1,59 @@
     4.4  signature Rules_sig =
     4.5  sig
     4.6  (*  structure USyntax : USyntax_sig *)
     4.7 -  type Type
     4.8 -  type Preterm
     4.9 -  type Term
    4.10 -  type Thm
    4.11 -  type Tactic
    4.12    type 'a binding
    4.13  
    4.14 -  val dest_thm : Thm -> Preterm list * Preterm
    4.15 +  val dest_thm : thm -> term list * term
    4.16  
    4.17    (* Inference rules *)
    4.18 -  val REFL      :Term -> Thm
    4.19 -  val ASSUME    :Term -> Thm
    4.20 -  val MP        :Thm -> Thm -> Thm
    4.21 -  val MATCH_MP  :Thm -> Thm -> Thm
    4.22 -  val CONJUNCT1 :Thm -> Thm
    4.23 -  val CONJUNCT2 :Thm -> Thm
    4.24 -  val CONJUNCTS :Thm -> Thm list
    4.25 -  val DISCH     :Term -> Thm -> Thm
    4.26 -  val UNDISCH   :Thm  -> Thm
    4.27 -  val INST_TYPE :Type binding list -> Thm -> Thm
    4.28 -  val SPEC      :Term -> Thm -> Thm
    4.29 -  val ISPEC     :Term -> Thm -> Thm
    4.30 -  val ISPECL    :Term list -> Thm -> Thm
    4.31 -  val GEN       :Term -> Thm -> Thm
    4.32 -  val GENL      :Term list -> Thm -> Thm
    4.33 -  val BETA_RULE :Thm -> Thm
    4.34 -  val LIST_CONJ :Thm list -> Thm
    4.35 +  val REFL      :cterm -> thm
    4.36 +  val ASSUME    :cterm -> thm
    4.37 +  val MP        :thm -> thm -> thm
    4.38 +  val MATCH_MP  :thm -> thm -> thm
    4.39 +  val CONJUNCT1 :thm -> thm
    4.40 +  val CONJUNCT2 :thm -> thm
    4.41 +  val CONJUNCTS :thm -> thm list
    4.42 +  val DISCH     :cterm -> thm -> thm
    4.43 +  val UNDISCH   :thm  -> thm
    4.44 +  val INST_TYPE :typ binding list -> thm -> thm
    4.45 +  val SPEC      :cterm -> thm -> thm
    4.46 +  val ISPEC     :cterm -> thm -> thm
    4.47 +  val ISPECL    :cterm list -> thm -> thm
    4.48 +  val GEN       :cterm -> thm -> thm
    4.49 +  val GENL      :cterm list -> thm -> thm
    4.50 +  val LIST_CONJ :thm list -> thm
    4.51  
    4.52 -  val SYM : Thm -> Thm
    4.53 -  val DISCH_ALL : Thm -> Thm
    4.54 -  val FILTER_DISCH_ALL : (Preterm -> bool) -> Thm -> Thm
    4.55 -  val SPEC_ALL  : Thm -> Thm
    4.56 -  val GEN_ALL   : Thm -> Thm
    4.57 -  val IMP_TRANS : Thm -> Thm -> Thm
    4.58 -  val PROVE_HYP : Thm -> Thm -> Thm
    4.59 +  val SYM : thm -> thm
    4.60 +  val DISCH_ALL : thm -> thm
    4.61 +  val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm
    4.62 +  val SPEC_ALL  : thm -> thm
    4.63 +  val GEN_ALL   : thm -> thm
    4.64 +  val IMP_TRANS : thm -> thm -> thm
    4.65 +  val PROVE_HYP : thm -> thm -> thm
    4.66  
    4.67 -  val CHOOSE : Term * Thm -> Thm -> Thm
    4.68 -  val EXISTS : Term * Term -> Thm -> Thm
    4.69 -  val EXISTL : Term list -> Thm -> Thm
    4.70 -  val IT_EXISTS : Term binding list -> Thm -> Thm
    4.71 +  val CHOOSE : cterm * thm -> thm -> thm
    4.72 +  val EXISTS : cterm * cterm -> thm -> thm
    4.73 +  val EXISTL : cterm list -> thm -> thm
    4.74 +  val IT_EXISTS : cterm binding list -> thm -> thm
    4.75  
    4.76 -  val EVEN_ORS : Thm list -> Thm list
    4.77 -  val DISJ_CASESL : Thm -> Thm list -> Thm
    4.78 +  val EVEN_ORS : thm list -> thm list
    4.79 +  val DISJ_CASESL : thm -> thm list -> thm
    4.80  
    4.81 -  val SUBS : Thm list -> Thm -> Thm
    4.82 -  val simplify : Thm list -> Thm -> Thm
    4.83 -  val simpl_conv : Thm list -> Term -> Thm
    4.84 +  val SUBS : thm list -> thm -> thm
    4.85 +  val simplify : thm list -> thm -> thm
    4.86 +  val simpl_conv : thm list -> cterm -> thm
    4.87  
    4.88  (* For debugging my isabelle solver in the conditional rewriter *)
    4.89  (*
    4.90 -  val term_ref : Preterm list ref
    4.91 -  val thm_ref : Thm list ref
    4.92 +  val term_ref : term list ref
    4.93 +  val thm_ref : thm list ref
    4.94    val mss_ref : meta_simpset list ref
    4.95    val tracing :bool ref
    4.96  *)
    4.97 -  val CONTEXT_REWRITE_RULE : Preterm * Preterm
    4.98 -                             -> {thms:Thm list,congs: Thm list, th:Thm} 
    4.99 -                             -> Thm * Preterm list
   4.100 -  val RIGHT_ASSOC : Thm -> Thm 
   4.101 +  val CONTEXT_REWRITE_RULE : term * term
   4.102 +                             -> {thms:thm list,congs: thm list, th:thm} 
   4.103 +                             -> thm * term list
   4.104 +  val RIGHT_ASSOC : thm -> thm 
   4.105  
   4.106 -  val prove : Term * Tactic -> Thm
   4.107 +  val prove : cterm * tactic -> thm
   4.108  end;
     5.1 --- a/TFL/sys.sml	Tue May 20 11:47:33 1997 +0200
     5.2 +++ b/TFL/sys.sml	Tue May 20 11:49:57 1997 +0200
     5.3 @@ -7,7 +7,6 @@
     5.4  
     5.5  (* Establish a base of common and/or helpful functions. *)
     5.6  use "utils.sig";
     5.7 -use "utils.sml";
     5.8  
     5.9  (* Get the specifications - these are independent of any system *)
    5.10  use "usyntax.sig";
    5.11 @@ -23,16 +22,16 @@
    5.12  
    5.13  use "tfl.sml";
    5.14  
    5.15 -structure Utils = UTILS(val int_to_string = string_of_int);
    5.16 +use "utils.sml";
    5.17  
    5.18  (*----------------------------------------------------------------------------
    5.19   *      Supply implementations
    5.20   *---------------------------------------------------------------------------*)
    5.21  
    5.22 -(* Ignore "Time" exception raised at end of building theory. *)
    5.23  use "usyntax.sml";
    5.24  use "thms.sml";
    5.25 -use"dcterm.sml"; use"rules.new.sml";
    5.26 +use"dcterm.sml"; 
    5.27 +use"rules.new.sml";
    5.28  use "thry.sml";
    5.29  
    5.30  
     6.1 --- a/TFL/tfl.sig	Tue May 20 11:47:33 1997 +0200
     6.2 +++ b/TFL/tfl.sig	Tue May 20 11:49:57 1997 +0200
     6.3 @@ -5,57 +5,51 @@
     6.4     structure Thry : Thry_sig
     6.5     structure USyntax : USyntax_sig
     6.6  
     6.7 -   type Preterm
     6.8 -   type Term
     6.9 -   type Thm
    6.10 -   type Thry
    6.11 -   type Tactic
    6.12 -   
    6.13 -   datatype pattern = GIVEN of Preterm * int
    6.14 -                    | OMITTED of Preterm * int
    6.15 +   datatype pattern = GIVEN of term * int
    6.16 +                    | OMITTED of term * int
    6.17  
    6.18 -   val mk_functional : Thry -> Preterm
    6.19 -                       -> {functional:Preterm,
    6.20 +   val mk_functional : theory -> term
    6.21 +                       -> {functional:term,
    6.22                             pats: pattern list}
    6.23  
    6.24 -   val wfrec_definition0 : Thry -> Preterm -> Preterm -> Thm * Thry
    6.25 +   val wfrec_definition0 : theory -> term -> term -> thm * theory
    6.26  
    6.27 -   val post_definition : Thry * (Thm * pattern list)
    6.28 -                              -> {theory : Thry,
    6.29 -                                  rules  : Thm, 
    6.30 -                                    TCs  : Preterm list list,
    6.31 -                          full_pats_TCs  : (Preterm * Preterm list) list, 
    6.32 +   val post_definition : theory * (thm * pattern list)
    6.33 +                              -> {theory : theory,
    6.34 +                                  rules  : thm, 
    6.35 +                                    TCs  : term list list,
    6.36 +                          full_pats_TCs  : (term * term list) list, 
    6.37                                 patterns  : pattern list}
    6.38  
    6.39  
    6.40 -   val wfrec_eqns : Thry -> Preterm
    6.41 -                     -> {WFR : Preterm, 
    6.42 -                         proto_def : Preterm,
    6.43 -                         extracta :(Thm * Preterm list) list,
    6.44 +   val wfrec_eqns : theory -> term
    6.45 +                     -> {WFR : term, 
    6.46 +                         proto_def : term,
    6.47 +                         extracta :(thm * term list) list,
    6.48                           pats  : pattern list}
    6.49  
    6.50  
    6.51 -   val lazyR_def : Thry
    6.52 -                   -> Preterm
    6.53 -                   -> {theory:Thry,
    6.54 -                       rules :Thm,
    6.55 -                           R :Preterm,
    6.56 -                       full_pats_TCs :(Preterm * Preterm list) list, 
    6.57 +   val lazyR_def : theory
    6.58 +                   -> term
    6.59 +                   -> {theory:theory,
    6.60 +                       rules :thm,
    6.61 +                           R :term,
    6.62 +                       full_pats_TCs :(term * term list) list, 
    6.63                         patterns: pattern list}
    6.64  
    6.65 -   val mk_induction : Thry 
    6.66 -                       -> Preterm -> Preterm 
    6.67 -                         -> (Preterm * Preterm list) list
    6.68 -                           -> Thm
    6.69 +   val mk_induction : theory 
    6.70 +                       -> term -> term 
    6.71 +                         -> (term * term list) list
    6.72 +                           -> thm
    6.73  
    6.74 -   val postprocess: {WFtac:Tactic, terminator:Tactic, simplifier:Term -> Thm}
    6.75 -                     -> Thry 
    6.76 -                      -> {rules:Thm, induction:Thm, TCs:Preterm list list}
    6.77 -                       -> {rules:Thm, induction:Thm, nested_tcs:Thm list}
    6.78 +   val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm}
    6.79 +                     -> theory 
    6.80 +                      -> {rules:thm, induction:thm, TCs:term list list}
    6.81 +                       -> {rules:thm, induction:thm, nested_tcs:thm list}
    6.82  
    6.83     structure Context
    6.84       : sig
    6.85 -         val read : unit -> Thm list
    6.86 -         val write : Thm list -> unit
    6.87 +         val read : unit -> thm list
    6.88 +         val write : thm list -> unit
    6.89         end
    6.90  end;
     7.1 --- a/TFL/tfl.sml	Tue May 20 11:47:33 1997 +0200
     7.2 +++ b/TFL/tfl.sml	Tue May 20 11:49:57 1997 +0200
     7.3 @@ -2,11 +2,7 @@
     7.4              structure Thry  : Thry_sig
     7.5              structure Thms  : Thms_sig
     7.6              sharing type Rules.binding = Thry.binding = 
     7.7 -                         Thry.USyntax.binding = Mask.binding
     7.8 -            sharing type Rules.Type = Thry.Type = Thry.USyntax.Type
     7.9 -            sharing type Rules.Preterm = Thry.Preterm = Thry.USyntax.Preterm
    7.10 -            sharing type Rules.Term = Thry.Term = Thry.USyntax.Term
    7.11 -            sharing type Thms.Thm = Rules.Thm = Thry.Thm) : TFL_sig  =
    7.12 +                         Thry.USyntax.binding = Mask.binding) : TFL_sig  =
    7.13  struct
    7.14  
    7.15  (* Declarations *)
    7.16 @@ -15,12 +11,6 @@
    7.17  structure Thry = Thry;
    7.18  structure USyntax = Thry.USyntax;
    7.19  
    7.20 -type Preterm = Thry.USyntax.Preterm;
    7.21 -type Term = Thry.USyntax.Term;
    7.22 -type Thm = Thms.Thm;
    7.23 -type Thry = Thry.Thry;
    7.24 -type Tactic = Rules.Tactic;
    7.25 -   
    7.26  
    7.27  (* Abbreviations *)
    7.28  structure R = Rules;
    7.29 @@ -30,22 +20,16 @@
    7.30  (* Declares 'a binding datatype *)
    7.31  open Mask;
    7.32  
    7.33 -nonfix mem --> |-> ##;
    7.34 +nonfix mem --> |->;
    7.35  val --> = S.-->;
    7.36 -val ##    = U.##;
    7.37  
    7.38  infixr 3 -->;
    7.39  infixr 7 |->;
    7.40 -infix  4 ##; 
    7.41  
    7.42  val concl = #2 o R.dest_thm;
    7.43  val hyp = #1 o R.dest_thm;
    7.44  
    7.45 -val list_mk_type = U.end_itlist (U.curry(op -->));
    7.46 -
    7.47 -fun flatten [] = []
    7.48 -  | flatten (h::t) = h@flatten t;
    7.49 -
    7.50 +val list_mk_type = U.end_itlist (curry(op -->));
    7.51  
    7.52  fun gtake f =
    7.53    let fun grab(0,rst) = ([],rst)
    7.54 @@ -59,8 +43,8 @@
    7.55   rev(#1(U.rev_itlist (fn x => fn (alist,i) => ((x,i)::alist, i+1)) L ([],0)));
    7.56  
    7.57  fun stringize [] = ""
    7.58 -  | stringize [i] = U.int_to_string i
    7.59 -  | stringize (h::t) = (U.int_to_string h^", "^stringize t);
    7.60 +  | stringize [i] = Int.toString i
    7.61 +  | stringize (h::t) = (Int.toString h^", "^stringize t);
    7.62  
    7.63  
    7.64  fun TFL_ERR{func,mesg} = U.ERR{module = "Tfl", func = func, mesg = mesg};
    7.65 @@ -78,12 +62,12 @@
    7.66  in
    7.67  fun gvvariant vlist =
    7.68    let val slist = ref (map (#Name o S.dest_var) vlist)
    7.69 -      val mem = U.mem (U.curry (op=))
    7.70 -      val _ = counter := 0
    7.71 +      val mem = U.mem (curry (op=))
    7.72 +      val dummy = counter := 0
    7.73        fun pass str = 
    7.74           if (mem str (!slist)) 
    7.75           then ( counter := !counter + 1;
    7.76 -                pass (U.concat"v" (U.int_to_string(!counter))))
    7.77 +                pass (U.concat"v" (Int.toString(!counter))))
    7.78           else (slist := str :: !slist; str)
    7.79    in 
    7.80    fn ty => S.mk_var{Name=pass "v",  Ty=ty}
    7.81 @@ -111,7 +95,7 @@
    7.82                       then ((args@rst, rhs)::in_group, not_in_group)
    7.83                       else (in_group, row::not_in_group)
    7.84                    end)      rows ([],[])
    7.85 -              val col_types = U.take S.type_of (length L, #1(hd in_group))
    7.86 +              val col_types = U.take type_of (length L, #1(hd in_group))
    7.87            in 
    7.88            part{constrs = crst, rows = not_in_group, 
    7.89                 A = {constructor = c, 
    7.90 @@ -127,8 +111,8 @@
    7.91   * This datatype carries some information about the origin of a
    7.92   * clause in a function definition.
    7.93   *---------------------------------------------------------------------------*)
    7.94 -datatype pattern = GIVEN   of S.Preterm * int
    7.95 -                 | OMITTED of S.Preterm * int
    7.96 +datatype pattern = GIVEN   of term * int
    7.97 +                 | OMITTED of term * int
    7.98  
    7.99  fun psubst theta (GIVEN (tm,i)) = GIVEN(S.subst theta tm, i)
   7.100    | psubst theta (OMITTED (tm,i)) = OMITTED(S.subst theta tm, i);
   7.101 @@ -195,13 +179,13 @@
   7.102   * Misc. routines used in mk_case
   7.103   *---------------------------------------------------------------------------*)
   7.104  
   7.105 -fun mk_pat c =
   7.106 -  let val L = length(#1(S.strip_type(S.type_of c)))
   7.107 +fun mk_pat (c,l) =
   7.108 +  let val L = length(#1(S.strip_type(type_of c)))
   7.109        fun build (prefix,tag,plist) =
   7.110 -          let val (args,plist') = gtake U.I (L, plist)
   7.111 -           in (prefix,tag,S.list_mk_comb(c,args)::plist') end
   7.112 -  in map build 
   7.113 -  end;
   7.114 +          let val args   = take (L,plist)
   7.115 +              and plist' = drop(L,plist)
   7.116 +          in (prefix,tag,list_comb(c,args)::plist') end
   7.117 +  in map build l end;
   7.118  
   7.119  fun v_to_prefix (prefix, v::pats) = (v::prefix,pats)
   7.120    | v_to_prefix _ = raise TFL_ERR{func="mk_case", mesg="v_to_prefix"};
   7.121 @@ -228,7 +212,7 @@
   7.122         if (S.is_var p) 
   7.123         then let val fresh = fresh_constr ty_match ty fresh_var
   7.124                  fun expnd (c,gvs) = 
   7.125 -                  let val capp = S.list_mk_comb(c,gvs)
   7.126 +                  let val capp = list_comb(c,gvs)
   7.127                    in ((prefix, capp::rst), psubst[p |-> capp] rhs)
   7.128                    end
   7.129              in map expnd (map fresh constructors)  end
   7.130 @@ -241,41 +225,44 @@
   7.131     | mk{path=[], rows = _::_} = mk_case_fail"blunder"
   7.132     | mk{path as u::rstp, rows as ((prefix, []), rhs)::rst} = 
   7.133          mk{path = path, 
   7.134 -           rows = ((prefix, [fresh_var(S.type_of u)]), rhs)::rst}
   7.135 +           rows = ((prefix, [fresh_var(type_of u)]), rhs)::rst}
   7.136     | mk{path = u::rstp, rows as ((_, p::_), _)::_} =
   7.137 -     let val (pat_rectangle,rights) = U.unzip rows
   7.138 +     let val (pat_rectangle,rights) = ListPair.unzip rows
   7.139           val col0 = map(hd o #2) pat_rectangle
   7.140       in 
   7.141 -     if (U.all S.is_var col0) 
   7.142 -     then let val rights' = map(fn(v,e) => psubst[v|->u] e) (U.zip col0 rights)
   7.143 +     if (forall S.is_var col0) 
   7.144 +     then let val rights' = map (fn(v,e) => psubst[v|->u] e)
   7.145 +                                (ListPair.zip (col0, rights))
   7.146                val pat_rectangle' = map v_to_prefix pat_rectangle
   7.147                val (pref_patl,tm) = mk{path = rstp,
   7.148 -                                      rows = U.zip pat_rectangle' rights'}
   7.149 +                                      rows = ListPair.zip (pat_rectangle',
   7.150 +                                                           rights')}
   7.151            in (map v_to_pats pref_patl, tm)
   7.152            end
   7.153       else
   7.154 -     let val pty = S.type_of p
   7.155 -         val ty_name = (#Tyop o S.dest_type) pty
   7.156 +     let val pty as Type (ty_name,_) = type_of p
   7.157       in
   7.158       case (ty_info ty_name)
   7.159 -     of U.NONE => mk_case_fail("Not a known datatype: "^ty_name)
   7.160 -      | U.SOME{case_const,constructors} =>
   7.161 +     of None => mk_case_fail("Not a known datatype: "^ty_name)
   7.162 +      | Some{case_const,constructors} =>
   7.163          let val case_const_name = #Name(S.dest_const case_const)
   7.164 -            val nrows = flatten (map (expand constructors pty) rows)
   7.165 +            val nrows = List_.concat (map (expand constructors pty) rows)
   7.166              val subproblems = divide(constructors, pty, range_ty, nrows)
   7.167              val groups      = map #group subproblems
   7.168              and new_formals = map #new_formals subproblems
   7.169              and constructors' = map #constructor subproblems
   7.170              val news = map (fn (nf,rows) => {path = nf@rstp, rows=rows})
   7.171 -                           (U.zip new_formals groups)
   7.172 +                           (ListPair.zip (new_formals, groups))
   7.173              val rec_calls = map mk news
   7.174 -            val (pat_rect,dtrees) = U.unzip rec_calls
   7.175 -            val case_functions = map S.list_mk_abs(U.zip new_formals dtrees)
   7.176 -            val types = map S.type_of (case_functions@[u]) @ [range_ty]
   7.177 +            val (pat_rect,dtrees) = ListPair.unzip rec_calls
   7.178 +            val case_functions = map S.list_mk_abs
   7.179 +                                  (ListPair.zip (new_formals, dtrees))
   7.180 +            val types = map type_of (case_functions@[u]) @ [range_ty]
   7.181              val case_const' = S.mk_const{Name = case_const_name,
   7.182                                           Ty   = list_mk_type types}
   7.183 -            val tree = S.list_mk_comb(case_const', case_functions@[u])
   7.184 -            val pat_rect1 = flatten(U.map2 mk_pat constructors' pat_rect)
   7.185 +            val tree = list_comb(case_const', case_functions@[u])
   7.186 +            val pat_rect1 = List_.concat
   7.187 +                              (ListPair.map mk_pat (constructors', pat_rect))
   7.188          in (pat_rect1,tree)
   7.189          end 
   7.190       end end
   7.191 @@ -307,24 +294,26 @@
   7.192        and paired2{Rator,Rand} = (Rator,Rand)
   7.193        fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s}
   7.194        fun single [f] = f
   7.195 -	| single fs  = mk_functional_err (Int.toString (length fs) ^ 
   7.196 -					  " distinct function names!")
   7.197 +        | single fs  = mk_functional_err (Int.toString (length fs) ^ 
   7.198 +                                          " distinct function names!")
   7.199  in
   7.200  fun mk_functional thy eqs =
   7.201   let val clauses = S.strip_conj eqs
   7.202 -     val (L,R) = U.unzip (map (paired1 o S.dest_eq o U.snd o S.strip_forall)
   7.203 -                              clauses)
   7.204 -     val (funcs,pats) = U.unzip(map (paired2 o S.dest_comb) L)
   7.205 +     val (L,R) = ListPair.unzip 
   7.206 +                    (map (paired1 o S.dest_eq o #2 o S.strip_forall)
   7.207 +                         clauses)
   7.208 +     val (funcs,pats) = ListPair.unzip(map (paired2 o S.dest_comb) L)
   7.209       val f = single (U.mk_set (S.aconv) funcs)
   7.210       val fvar = if (S.is_var f) then f else S.mk_var(S.dest_const f)
   7.211 -     val _ = map (no_repeat_vars thy) pats
   7.212 -     val rows = U.zip (map (fn x => ([],[x])) pats) (map GIVEN (enumerate R))
   7.213 +     val dummy = map (no_repeat_vars thy) pats
   7.214 +     val rows = ListPair.zip (map (fn x => ([],[x])) pats,
   7.215 +                              map GIVEN (enumerate R))
   7.216       val fvs = S.free_varsl R
   7.217 -     val a = S.variant fvs (S.mk_var{Name="a", Ty = S.type_of(hd pats)})
   7.218 +     val a = S.variant fvs (S.mk_var{Name="a", Ty = type_of(hd pats)})
   7.219       val FV = a::fvs
   7.220       val ty_info = Thry.match_info thy
   7.221       val ty_match = Thry.match_type thy
   7.222 -     val range_ty = S.type_of (hd R)
   7.223 +     val range_ty = type_of (hd R)
   7.224       val (patts, case_tm) = mk_case ty_info ty_match FV range_ty 
   7.225                                      {path=[a], rows=rows}
   7.226       val patts1 = map (fn (_,(tag,i),[pat]) => tag (pat,i)) patts handle _ 
   7.227 @@ -333,7 +322,7 @@
   7.228       val finals = map row_of_pat patts2
   7.229       val originals = map (row_of_pat o #2) rows
   7.230       fun int_eq i1 (i2:int) =  (i1=i2)
   7.231 -     val _ = case (U.set_diff int_eq originals finals)
   7.232 +     val dummy = case (U.set_diff int_eq originals finals)
   7.233               of [] => ()
   7.234            | L => mk_functional_err("The following rows (counting from zero)\
   7.235                                     \ are inaccessible: "^stringize L)
   7.236 @@ -365,8 +354,8 @@
   7.237       val def_name = U.concat Name "_def"
   7.238       val (_,ty_theta) = Thry.match_term thy f (S.mk_var{Name=fname,Ty=Ty})
   7.239       val wfrec' = S.inst ty_theta wfrec
   7.240 -     val wfrec_R_M' = S.list_mk_comb(wfrec',[R,functional])
   7.241 -     val def_term = S.mk_eq{lhs=Bvar, rhs=wfrec_R_M'}
   7.242 +     val wfrec_R_M' = list_comb(wfrec',[R,functional])
   7.243 +     val def_term = HOLogic.mk_eq(Bvar, wfrec_R_M')
   7.244    in 
   7.245    Thry.make_definition thy def_name def_term
   7.246    end
   7.247 @@ -380,7 +369,7 @@
   7.248   *---------------------------------------------------------------------------*)
   7.249  structure Context =
   7.250  struct
   7.251 -  val non_datatype_context = ref []:Rules.Thm list ref
   7.252 +  val non_datatype_context = ref []: thm list ref
   7.253    fun read() = !non_datatype_context
   7.254    fun write L = (non_datatype_context := L)
   7.255  end;
   7.256 @@ -430,14 +419,14 @@
   7.257                           {thms = [(R.ISPECL o map tych)[f,R] Thms.CUT_LEMMA],
   7.258                           congs = context_congs,
   7.259                              th = th}
   7.260 -     val (rules, TCs) = U.unzip (map xtract corollaries')
   7.261 +     val (rules, TCs) = ListPair.unzip (map xtract corollaries')
   7.262       val rules0 = map (R.simplify [Thms.CUT_DEF]) rules
   7.263       val mk_cond_rule = R.FILTER_DISCH_ALL(not o S.aconv WFR)
   7.264       val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
   7.265   in
   7.266   {theory = theory,   (* holds def, if it's needed *)
   7.267    rules = rules1,
   7.268 -  full_pats_TCs = merge (map pat_of pats) (U.zip given_pats TCs), 
   7.269 +  full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)), 
   7.270    TCs = TCs, 
   7.271    patterns = pats}
   7.272   end;
   7.273 @@ -452,8 +441,7 @@
   7.274       val given_pats = givens pats
   7.275       val {Bvar = f, Body} = S.dest_abs functional
   7.276       val {Bvar = x, ...} = S.dest_abs Body
   7.277 -     val {Name,Ty = fty} = S.dest_var f
   7.278 -     val {Tyop="fun", Args = [f_dty, f_rty]} = S.dest_type fty
   7.279 +     val {Name, Ty = Type("fun", [f_dty, f_rty])} = S.dest_var f
   7.280       val (case_rewrites,context_congs) = extraction_thms thy
   7.281       val tych = Thry.typecheck thy
   7.282       val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
   7.283 @@ -487,8 +475,8 @@
   7.284       val R1 = S.rand WFR
   7.285       val f = S.lhs proto_def
   7.286       val {Name,...} = S.dest_var f
   7.287 -     val (extractants,TCl) = U.unzip extracta
   7.288 -     val TCs = U.Union S.aconv TCl
   7.289 +     val (extractants,TCl) = ListPair.unzip extracta
   7.290 +     val TCs = foldr (gen_union (op aconv)) (TCl, [])
   7.291       val full_rqt = WFR::TCs
   7.292       val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
   7.293       val R'abs = S.rand R'
   7.294 @@ -502,11 +490,11 @@
   7.295                               (R.SPEC (tych R') (R.GENL[tych R1, tych f] baz)))
   7.296                       def
   7.297       val body_th = R.LIST_CONJ (map (R.ASSUME o tych) full_rqt)
   7.298 -     val bar = R.MP (R.BETA_RULE(R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX))
   7.299 +     val bar = R.MP (R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX)
   7.300                      body_th
   7.301   in {theory = theory, R=R1,
   7.302       rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def',
   7.303 -     full_pats_TCs = merge (map pat_of pats) (U.zip (givens pats) TCl),
   7.304 +     full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
   7.305       patterns = pats}
   7.306   end;
   7.307  
   7.308 @@ -538,22 +526,21 @@
   7.309   * pairing the incoming new variable with the term it gets beta-reduced into.
   7.310   *---------------------------------------------------------------------------*)
   7.311  
   7.312 -fun alpha_ex_unroll xlist tm =
   7.313 +fun alpha_ex_unroll (xlist, tm) =
   7.314    let val (qvars,body) = S.strip_exists tm
   7.315        val vlist = #2(S.strip_comb (S.rhs body))
   7.316 -      val plist = U.zip vlist xlist
   7.317 -      val args = map (U.C (U.assoc1 (U.uncurry S.aconv)) plist) qvars
   7.318 -      val args' = map (fn U.SOME(_,v) => v 
   7.319 -                        | U.NONE => raise TFL_ERR{func = "alpha_ex_unroll",
   7.320 -                                       mesg = "no correspondence"}) args
   7.321 +      val plist = ListPair.zip (vlist, xlist)
   7.322 +      val args = map (fn qv => the (gen_assoc (op aconv) (plist, qv))) qvars
   7.323 +                   handle OPTION _ => error 
   7.324 +                       "TFL fault [alpha_ex_unroll]: no correspondence"
   7.325        fun build ex [] = []
   7.326          | build ex (v::rst) =
   7.327             let val ex1 = S.beta_conv(S.mk_comb{Rator=S.rand ex, Rand=v})
   7.328             in ex1::build ex1 rst
   7.329             end
   7.330 -     val (nex::exl) = rev (tm::build tm args')
   7.331 +     val (nex::exl) = rev (tm::build tm args)
   7.332    in 
   7.333 -  (nex, U.zip args' (rev exl))
   7.334 +  (nex, ListPair.zip (args, rev exl))
   7.335    end;
   7.336  
   7.337  
   7.338 @@ -574,27 +561,28 @@
   7.339     | mk{path=[], rows = [([], (thm, bindings))]} = 
   7.340                           R.IT_EXISTS (map tych_binding bindings) thm
   7.341     | mk{path = u::rstp, rows as (p::_, _)::_} =
   7.342 -     let val (pat_rectangle,rights) = U.unzip rows
   7.343 +     let val (pat_rectangle,rights) = ListPair.unzip rows
   7.344           val col0 = map hd pat_rectangle
   7.345           val pat_rectangle' = map tl pat_rectangle
   7.346       in 
   7.347 -     if (U.all S.is_var col0) (* column 0 is all variables *)
   7.348 +     if (forall S.is_var col0) (* column 0 is all variables *)
   7.349       then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[u|->v]))
   7.350 -                                (U.zip rights col0)
   7.351 -          in mk{path = rstp, rows = U.zip pat_rectangle' rights'}
   7.352 +                                (ListPair.zip (rights, col0))
   7.353 +          in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}
   7.354            end
   7.355       else                     (* column 0 is all constructors *)
   7.356 -     let val ty_name = (#Tyop o S.dest_type o S.type_of) p
   7.357 +     let val Type (ty_name,_) = type_of p
   7.358       in
   7.359       case (ty_info ty_name)
   7.360 -     of U.NONE => fail("Not a known datatype: "^ty_name)
   7.361 -      | U.SOME{constructors,nchotomy} =>
   7.362 +     of None => fail("Not a known datatype: "^ty_name)
   7.363 +      | Some{constructors,nchotomy} =>
   7.364          let val thm' = R.ISPEC (tych u) nchotomy
   7.365              val disjuncts = S.strip_disj (concl thm')
   7.366              val subproblems = divide(constructors, rows)
   7.367              val groups      = map #group subproblems
   7.368              and new_formals = map #new_formals subproblems
   7.369 -            val existentials = U.map2 alpha_ex_unroll new_formals disjuncts
   7.370 +            val existentials = ListPair.map alpha_ex_unroll
   7.371 +                                   (new_formals, disjuncts)
   7.372              val constraints = map #1 existentials
   7.373              val vexl = map #2 existentials
   7.374              fun expnd tm (pats,(th,b)) = (pats,(R.SUBS[R.ASSUME(tych tm)]th,b))
   7.375 @@ -602,8 +590,10 @@
   7.376                                                 rows = map (expnd c) rows})
   7.377                             (U.zip3 new_formals groups constraints)
   7.378              val recursive_thms = map mk news
   7.379 -            val build_exists = U.itlist(R.CHOOSE o (tych##(R.ASSUME o tych)))
   7.380 -            val thms' = U.map2 build_exists vexl recursive_thms
   7.381 +            val build_exists = foldr
   7.382 +                                (fn((x,t), th) => 
   7.383 +                                 R.CHOOSE (tych x, R.ASSUME (tych t)) th)
   7.384 +            val thms' = ListPair.map build_exists (vexl, recursive_thms)
   7.385              val same_concls = R.EVEN_ORS thms'
   7.386          in R.DISJ_CASESL thm' same_concls
   7.387          end 
   7.388 @@ -618,11 +608,11 @@
   7.389       val ty_info = Thry.induct_info thy
   7.390   in fn pats =>
   7.391   let val FV0 = S.free_varsl pats
   7.392 -     val a = S.variant FV0 (pmk_var "a" (S.type_of(hd pats)))
   7.393 -     val v = S.variant (a::FV0) (pmk_var "v" (S.type_of a))
   7.394 +     val a = S.variant FV0 (pmk_var "a" (type_of(hd pats)))
   7.395 +     val v = S.variant (a::FV0) (pmk_var "v" (type_of a))
   7.396       val FV = a::v::FV0
   7.397 -     val a_eq_v = S.mk_eq{lhs = a, rhs = v}
   7.398 -     val ex_th0 = R.EXISTS ((tych##tych) (S.mk_exists{Bvar=v,Body=a_eq_v},a))
   7.399 +     val a_eq_v = HOLogic.mk_eq(a,v)
   7.400 +     val ex_th0 = R.EXISTS (tych (S.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
   7.401                             (R.REFL (tych a))
   7.402       val th0 = R.ASSUME (tych a_eq_v)
   7.403       val rows = map (fn x => ([x], (th0,[]))) pats
   7.404 @@ -665,7 +655,7 @@
   7.405           end
   7.406   in case TCs
   7.407      of [] => (S.list_mk_forall(globals, P^pat), [])
   7.408 -     |  _ => let val (ihs, TCs_locals) = U.unzip(map dest_TC TCs)
   7.409 +     |  _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
   7.410                   val ind_clause = S.list_mk_conj ihs ==> P^pat
   7.411               in (S.list_mk_forall(globals,ind_clause), TCs_locals)
   7.412               end
   7.413 @@ -725,15 +715,13 @@
   7.414          let val ex_tm = S.mk_exists{Bvar=v,Body=tm}
   7.415          in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm)
   7.416          end
   7.417 -      val [veq] = U.filter (U.can S.dest_eq) (#1 (R.dest_thm thm))
   7.418 +      val [veq] = filter (U.can S.dest_eq) (#1 (R.dest_thm thm))
   7.419        val {lhs,rhs} = S.dest_eq veq
   7.420        val L = S.free_vars_lr rhs
   7.421 -  in U.snd(U.itlist CHOOSER L (veq,thm))
   7.422 -  end;
   7.423 +  in  #2 (U.itlist CHOOSER L (veq,thm))  end;
   7.424  
   7.425  
   7.426  fun combize M N = S.mk_comb{Rator=M,Rand=N};
   7.427 -fun eq v tm = S.mk_eq{lhs=v,rhs=tm};
   7.428  
   7.429  
   7.430  (*----------------------------------------------------------------------------
   7.431 @@ -746,15 +734,15 @@
   7.432  fun mk_induction thy f R pat_TCs_list =
   7.433  let val tych = Thry.typecheck thy
   7.434      val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM)
   7.435 -    val (pats,TCsl) = U.unzip pat_TCs_list
   7.436 +    val (pats,TCsl) = ListPair.unzip pat_TCs_list
   7.437      val case_thm = complete_cases thy pats
   7.438 -    val domain = (S.type_of o hd) pats
   7.439 -    val P = S.variant (S.all_varsl (pats@flatten TCsl))
   7.440 -                      (S.mk_var{Name="P", Ty=domain --> S.bool})
   7.441 +    val domain = (type_of o hd) pats
   7.442 +    val P = S.variant (S.all_varsl (pats @ List_.concat TCsl))
   7.443 +                      (S.mk_var{Name="P", Ty=domain --> HOLogic.boolT})
   7.444      val Sinduct = R.SPEC (tych P) Sinduction
   7.445      val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
   7.446      val Rassums_TCl' = map (build_ih f P) pat_TCs_list
   7.447 -    val (Rassums,TCl') = U.unzip Rassums_TCl'
   7.448 +    val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
   7.449      val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
   7.450      val cases = map (S.beta_conv o combize Sinduct_assumf) pats
   7.451      val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
   7.452 @@ -762,12 +750,13 @@
   7.453      val v = S.variant (S.free_varsl (map concl proved_cases))
   7.454                        (S.mk_var{Name="v", Ty=domain})
   7.455      val vtyped = tych v
   7.456 -    val substs = map (R.SYM o R.ASSUME o tych o eq v) pats
   7.457 -    val proved_cases1 = U.map2 (fn th => R.SUBS[th]) substs proved_cases
   7.458 +    val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
   7.459 +    val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th') 
   7.460 +                          (substs, proved_cases)
   7.461      val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1
   7.462      val dant = R.GEN vtyped (R.DISJ_CASESL (R.ISPEC vtyped case_thm) abs_cases)
   7.463      val dc = R.MP Sinduct dant
   7.464 -    val Parg_ty = S.type_of(#Bvar(S.dest_forall(concl dc)))
   7.465 +    val Parg_ty = type_of(#Bvar(S.dest_forall(concl dc)))
   7.466      val vars = map (gvvariant[P]) (S.strip_prod_type Parg_ty)
   7.467      val dc' = U.itlist (R.GEN o tych) vars
   7.468                         (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc)
   7.469 @@ -880,11 +869,10 @@
   7.470              val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1
   7.471          in loop(rst, nthms@extra_tc_thms, r2::R, ind1)
   7.472          end
   7.473 -   val rules_tcs = U.zip (R.CONJUNCTS rules1) TCs
   7.474 +   val rules_tcs = ListPair.zip (R.CONJUNCTS rules1, TCs)
   7.475     val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1)
   7.476  in
   7.477    {induction = ind2, rules = R.LIST_CONJ rules2, nested_tcs = extras}
   7.478  end;
   7.479  
   7.480 -
   7.481  end; (* TFL *)
     8.1 --- a/TFL/thms.sig	Tue May 20 11:47:33 1997 +0200
     8.2 +++ b/TFL/thms.sig	Tue May 20 11:49:57 1997 +0200
     8.3 @@ -1,16 +1,15 @@
     8.4  signature Thms_sig =
     8.5  sig
     8.6 -   type Thm
     8.7 -   val WF_INDUCTION_THM:Thm
     8.8 -   val WFREC_COROLLARY :Thm
     8.9 -   val CUT_DEF         :Thm
    8.10 -   val CUT_LEMMA       :Thm
    8.11 -   val SELECT_AX       :Thm
    8.12 +   val WF_INDUCTION_THM:thm
    8.13 +   val WFREC_COROLLARY :thm
    8.14 +   val CUT_DEF         :thm
    8.15 +   val CUT_LEMMA       :thm
    8.16 +   val SELECT_AX       :thm
    8.17     
    8.18 -   val COND_CONG :Thm
    8.19 -   val LET_CONG  :Thm
    8.20 +   val COND_CONG :thm
    8.21 +   val LET_CONG  :thm
    8.22  
    8.23 -   val eqT       :Thm
    8.24 -   val rev_eq_mp :Thm
    8.25 -   val simp_thm  :Thm
    8.26 +   val eqT       :thm
    8.27 +   val rev_eq_mp :thm
    8.28 +   val simp_thm  :thm
    8.29  end;
     9.1 --- a/TFL/thms.sml	Tue May 20 11:47:33 1997 +0200
     9.2 +++ b/TFL/thms.sml	Tue May 20 11:49:57 1997 +0200
     9.3 @@ -1,7 +1,5 @@
     9.4  structure Thms : Thms_sig =
     9.5  struct
     9.6 -   type Thm = Thm.thm
     9.7 -
     9.8     val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec"
     9.9     val WF_INDUCTION_THM = get_thm WF_Rel.thy "tfl_wf_induct"
    9.10     val CUT_LEMMA = get_thm WF_Rel.thy "tfl_cut_apply"
    10.1 --- a/TFL/thry.sig	Tue May 20 11:47:33 1997 +0200
    10.2 +++ b/TFL/thry.sig	Tue May 20 11:49:57 1997 +0200
    10.3 @@ -1,30 +1,25 @@
    10.4  signature Thry_sig =
    10.5  sig
    10.6 -  type Type
    10.7 -  type Preterm
    10.8 -  type Term
    10.9 -  type Thm
   10.10 -  type Thry
   10.11    type 'a binding
   10.12  
   10.13    structure USyntax : USyntax_sig
   10.14 -  val match_term : Thry -> Preterm -> Preterm 
   10.15 -                    -> Preterm binding list * Type binding list
   10.16 +  val match_term : theory -> term -> term 
   10.17 +                    -> term binding list * typ binding list
   10.18  
   10.19 -  val match_type : Thry -> Type -> Type -> Type binding list
   10.20 +  val match_type : theory -> typ -> typ -> typ binding list
   10.21  
   10.22 -  val typecheck : Thry -> Preterm -> Term
   10.23 +  val typecheck : theory -> term -> cterm
   10.24  
   10.25 -  val make_definition: Thry -> string -> Preterm -> Thm * Thry
   10.26 +  val make_definition: theory -> string -> term -> thm * theory
   10.27  
   10.28    (* Datatype facts of various flavours *)
   10.29 -  val match_info: Thry -> string -> {constructors:Preterm list,
   10.30 -                                     case_const:Preterm} USyntax.Utils.option
   10.31 +  val match_info: theory -> string -> {constructors:term list,
   10.32 +                                     case_const:term} option
   10.33  
   10.34 -  val induct_info: Thry -> string -> {constructors:Preterm list,
   10.35 -                                      nchotomy:Thm} USyntax.Utils.option
   10.36 +  val induct_info: theory -> string -> {constructors:term list,
   10.37 +                                      nchotomy:thm} option
   10.38  
   10.39 -  val extract_info: Thry -> {case_congs:Thm list, case_rewrites:Thm list}
   10.40 +  val extract_info: theory -> {case_congs:thm list, case_rewrites:thm list}
   10.41  
   10.42  end;
   10.43  
    11.1 --- a/TFL/thry.sml	Tue May 20 11:47:33 1997 +0200
    11.2 +++ b/TFL/thry.sml	Tue May 20 11:49:57 1997 +0200
    11.3 @@ -2,11 +2,6 @@
    11.4  struct
    11.5  
    11.6  structure USyntax  = USyntax;
    11.7 -type Type = USyntax.Type
    11.8 -type Preterm = USyntax.Preterm
    11.9 -type Term = USyntax.Term
   11.10 -type Thm = Thm.thm
   11.11 -type Thry = theory;
   11.12  
   11.13  open Mask;
   11.14  structure S = USyntax;
   11.15 @@ -66,9 +61,9 @@
   11.16         val {Name,Ty} = S.dest_var lhs
   11.17         val lhs1 = S.mk_const{Name = Name, Ty = Ty}
   11.18         val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop}
   11.19 -       val dtm = S.list_mk_comb(eeq1,[lhs1,rhs])      (* Rename "=" to "==" *)
   11.20 +       val dtm = list_comb(eeq1,[lhs1,rhs])      (* Rename "=" to "==" *)
   11.21         val (_, tm', _) = Sign.infer_types (sign_of parent)
   11.22 -	             (K None) (K None) [] true ([dtm],propT)
   11.23 +                     (K None) (K None) [] true ([dtm],propT)
   11.24         val new_thy = add_defs_i [(s,tm')] parent
   11.25     in 
   11.26     (freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy)
   11.27 @@ -112,24 +107,24 @@
   11.28   * is temporary, I hope!
   11.29   *---------------------------------------------------------------------------*)
   11.30  val match_info = fn thy =>
   11.31 -    fn "*" => Utils.SOME({case_const = #case_const (#2 prod_record),
   11.32 +    fn "*" => Some({case_const = #case_const (#2 prod_record),
   11.33                       constructors = #constructors (#2 prod_record)})
   11.34 -     | "nat" => Utils.SOME({case_const = #case_const (#2 nat_record),
   11.35 +     | "nat" => Some({case_const = #case_const (#2 nat_record),
   11.36                         constructors = #constructors (#2 nat_record)})
   11.37       | ty => case assoc(!datatypes,ty)
   11.38 -               of None => Utils.NONE
   11.39 +               of None => None
   11.40                  | Some{case_const,constructors, ...} =>
   11.41 -                   Utils.SOME{case_const=case_const, constructors=constructors}
   11.42 +                   Some{case_const=case_const, constructors=constructors}
   11.43  
   11.44  val induct_info = fn thy =>
   11.45 -    fn "*" => Utils.SOME({nchotomy = #nchotomy (#2 prod_record),
   11.46 +    fn "*" => Some({nchotomy = #nchotomy (#2 prod_record),
   11.47                       constructors = #constructors (#2 prod_record)})
   11.48 -     | "nat" => Utils.SOME({nchotomy = #nchotomy (#2 nat_record),
   11.49 +     | "nat" => Some({nchotomy = #nchotomy (#2 nat_record),
   11.50                         constructors = #constructors (#2 nat_record)})
   11.51       | ty => case assoc(!datatypes,ty)
   11.52 -               of None => Utils.NONE
   11.53 +               of None => None
   11.54                  | Some{nchotomy,constructors, ...} =>
   11.55 -                  Utils.SOME{nchotomy=nchotomy, constructors=constructors}
   11.56 +                  Some{nchotomy=nchotomy, constructors=constructors}
   11.57  
   11.58  val extract_info = fn thy => 
   11.59   let val case_congs = map (#case_cong o #2) (!datatypes)
   11.60 @@ -140,5 +135,4 @@
   11.61                       #case_rewrites(#2 nat_record)@case_rewrites}
   11.62   end;
   11.63  
   11.64 -
   11.65  end; (* Thry *)
    12.1 --- a/TFL/usyntax.sig	Tue May 20 11:47:33 1997 +0200
    12.2 +++ b/TFL/usyntax.sig	Tue May 20 11:49:57 1997 +0200
    12.3 @@ -2,133 +2,122 @@
    12.4  sig
    12.5    structure Utils : Utils_sig
    12.6  
    12.7 -  type Type
    12.8 -  type Term
    12.9 -  type Preterm
   12.10    type 'a binding
   12.11  
   12.12 -  datatype lambda = VAR   of {Name : string, Ty : Type}
   12.13 -                  | CONST of {Name : string, Ty : Type}
   12.14 -                  | COMB  of {Rator: Preterm, Rand : Preterm}
   12.15 -                  | LAMB  of {Bvar : Preterm, Body : Preterm}
   12.16 +  datatype lambda = VAR   of {Name : string, Ty : typ}
   12.17 +                  | CONST of {Name : string, Ty : typ}
   12.18 +                  | COMB  of {Rator: term, Rand : term}
   12.19 +                  | LAMB  of {Bvar : term, Body : term}
   12.20  
   12.21 -  val alpha : Type
   12.22 -  val bool  : Type
   12.23 -  val mk_preterm : Term -> Preterm
   12.24 -  val drop_Trueprop : Preterm -> Preterm
   12.25 +  val alpha : typ
   12.26 +  val mk_preterm : cterm -> term
   12.27  
   12.28    (* Types *)
   12.29 -  val type_vars  : Type -> Type list
   12.30 -  val type_varsl : Type list -> Type list
   12.31 -  val mk_type    : {Tyop: string, Args:Type list} -> Type
   12.32 -  val dest_type  : Type -> {Tyop : string, Args : Type list}
   12.33 -  val mk_vartype : string -> Type
   12.34 -  val is_vartype : Type -> bool
   12.35 -  val -->        : Type * Type -> Type
   12.36 -  val strip_type : Type -> Type list * Type
   12.37 -  val strip_prod_type : Type -> Type list
   12.38 -  val match_type: Type -> Type -> Type binding list
   12.39 +  val type_vars  : typ -> typ list
   12.40 +  val type_varsl : typ list -> typ list
   12.41 +  val mk_vartype : string -> typ
   12.42 +  val is_vartype : typ -> bool
   12.43 +  val -->        : typ * typ -> typ
   12.44 +  val strip_type : typ -> typ list * typ
   12.45 +  val strip_prod_type : typ -> typ list
   12.46 +  val match_type: typ -> typ -> typ binding list
   12.47  
   12.48    (* Terms *)
   12.49 -  val free_vars  : Preterm -> Preterm list
   12.50 -  val free_varsl : Preterm list -> Preterm list
   12.51 -  val free_vars_lr : Preterm -> Preterm list
   12.52 -  val all_vars   : Preterm -> Preterm list
   12.53 -  val all_varsl  : Preterm list -> Preterm list
   12.54 -  val variant    : Preterm list -> Preterm -> Preterm
   12.55 -  val type_of    : Preterm -> Type
   12.56 -  val type_vars_in_term : Preterm -> Type list
   12.57 -  val dest_term  : Preterm -> lambda
   12.58 +  val free_vars  : term -> term list
   12.59 +  val free_varsl : term list -> term list
   12.60 +  val free_vars_lr : term -> term list
   12.61 +  val all_vars   : term -> term list
   12.62 +  val all_varsl  : term list -> term list
   12.63 +  val variant    : term list -> term -> term
   12.64 +  val type_vars_in_term : term -> typ list
   12.65 +  val dest_term  : term -> lambda
   12.66    
   12.67    (* Prelogic *)
   12.68 -  val aconv     : Preterm -> Preterm -> bool
   12.69 -  val subst     : Preterm binding list -> Preterm -> Preterm
   12.70 -  val inst      : Type binding list -> Preterm -> Preterm
   12.71 -  val beta_conv : Preterm -> Preterm
   12.72 +  val aconv     : term -> term -> bool
   12.73 +  val subst     : term binding list -> term -> term
   12.74 +  val inst      : typ binding list -> term -> term
   12.75 +  val beta_conv : term -> term
   12.76  
   12.77    (* Construction routines *)
   12.78 -  val mk_prop   :Preterm -> Preterm
   12.79 -  val mk_var    :{Name : string, Ty : Type} -> Preterm
   12.80 -  val mk_const  :{Name : string, Ty : Type} -> Preterm
   12.81 -  val mk_comb   :{Rator : Preterm, Rand : Preterm} -> Preterm
   12.82 -  val mk_abs    :{Bvar  : Preterm, Body : Preterm} -> Preterm
   12.83 +  val mk_var    :{Name : string, Ty : typ} -> term
   12.84 +  val mk_const  :{Name : string, Ty : typ} -> term
   12.85 +  val mk_comb   :{Rator : term, Rand : term} -> term
   12.86 +  val mk_abs    :{Bvar  : term, Body : term} -> term
   12.87  
   12.88 -  val mk_eq     :{lhs : Preterm, rhs : Preterm} -> Preterm
   12.89 -  val mk_imp    :{ant : Preterm, conseq :  Preterm} -> Preterm
   12.90 -  val mk_select :{Bvar : Preterm, Body : Preterm} -> Preterm
   12.91 -  val mk_forall :{Bvar : Preterm, Body : Preterm} -> Preterm
   12.92 -  val mk_exists :{Bvar : Preterm, Body : Preterm} -> Preterm
   12.93 -  val mk_conj   :{conj1 : Preterm, conj2 : Preterm} -> Preterm
   12.94 -  val mk_disj   :{disj1 : Preterm, disj2 : Preterm} -> Preterm
   12.95 -  val mk_pabs   :{varstruct : Preterm, body : Preterm} -> Preterm
   12.96 +  val mk_imp    :{ant : term, conseq :  term} -> term
   12.97 +  val mk_select :{Bvar : term, Body : term} -> term
   12.98 +  val mk_forall :{Bvar : term, Body : term} -> term
   12.99 +  val mk_exists :{Bvar : term, Body : term} -> term
  12.100 +  val mk_conj   :{conj1 : term, conj2 : term} -> term
  12.101 +  val mk_disj   :{disj1 : term, disj2 : term} -> term
  12.102 +  val mk_pabs   :{varstruct : term, body : term} -> term
  12.103  
  12.104    (* Destruction routines *)
  12.105 -  val dest_var  : Preterm -> {Name : string, Ty : Type}
  12.106 -  val dest_const: Preterm -> {Name : string, Ty : Type}
  12.107 -  val dest_comb : Preterm -> {Rator : Preterm, Rand : Preterm}
  12.108 -  val dest_abs  : Preterm -> {Bvar : Preterm, Body : Preterm}
  12.109 -  val dest_eq     : Preterm -> {lhs : Preterm, rhs : Preterm}
  12.110 -  val dest_imp    : Preterm -> {ant : Preterm, conseq : Preterm}
  12.111 -  val dest_select : Preterm -> {Bvar : Preterm, Body : Preterm}
  12.112 -  val dest_forall : Preterm -> {Bvar : Preterm, Body : Preterm}
  12.113 -  val dest_exists : Preterm -> {Bvar : Preterm, Body : Preterm}
  12.114 -  val dest_neg    : Preterm -> Preterm
  12.115 -  val dest_conj   : Preterm -> {conj1 : Preterm, conj2 : Preterm}
  12.116 -  val dest_disj   : Preterm -> {disj1 : Preterm, disj2 : Preterm}
  12.117 -  val dest_pair   : Preterm -> {fst : Preterm, snd : Preterm}
  12.118 -  val dest_pabs   : Preterm -> {varstruct : Preterm, body : Preterm}
  12.119 +  val dest_var  : term -> {Name : string, Ty : typ}
  12.120 +  val dest_const: term -> {Name : string, Ty : typ}
  12.121 +  val dest_comb : term -> {Rator : term, Rand : term}
  12.122 +  val dest_abs  : term -> {Bvar : term, Body : term}
  12.123 +  val dest_eq     : term -> {lhs : term, rhs : term}
  12.124 +  val dest_imp    : term -> {ant : term, conseq : term}
  12.125 +  val dest_select : term -> {Bvar : term, Body : term}
  12.126 +  val dest_forall : term -> {Bvar : term, Body : term}
  12.127 +  val dest_exists : term -> {Bvar : term, Body : term}
  12.128 +  val dest_neg    : term -> term
  12.129 +  val dest_conj   : term -> {conj1 : term, conj2 : term}
  12.130 +  val dest_disj   : term -> {disj1 : term, disj2 : term}
  12.131 +  val dest_pair   : term -> {fst : term, snd : term}
  12.132 +  val dest_pabs   : term -> {varstruct : term, body : term}
  12.133  
  12.134 -  val lhs   : Preterm -> Preterm
  12.135 -  val rhs   : Preterm -> Preterm
  12.136 -  val rator : Preterm -> Preterm
  12.137 -  val rand  : Preterm -> Preterm
  12.138 -  val bvar  : Preterm -> Preterm
  12.139 -  val body  : Preterm -> Preterm
  12.140 +  val lhs   : term -> term
  12.141 +  val rhs   : term -> term
  12.142 +  val rator : term -> term
  12.143 +  val rand  : term -> term
  12.144 +  val bvar  : term -> term
  12.145 +  val body  : term -> term
  12.146    
  12.147  
  12.148    (* Query routines *)
  12.149 -  val is_var  : Preterm -> bool
  12.150 -  val is_const: Preterm -> bool
  12.151 -  val is_comb : Preterm -> bool
  12.152 -  val is_abs  : Preterm -> bool
  12.153 -  val is_eq     : Preterm -> bool
  12.154 -  val is_imp    : Preterm -> bool
  12.155 -  val is_forall : Preterm -> bool 
  12.156 -  val is_exists : Preterm -> bool 
  12.157 -  val is_neg    : Preterm -> bool
  12.158 -  val is_conj   : Preterm -> bool
  12.159 -  val is_disj   : Preterm -> bool
  12.160 -  val is_pair   : Preterm -> bool
  12.161 -  val is_pabs   : Preterm -> bool
  12.162 +  val is_var  : term -> bool
  12.163 +  val is_const: term -> bool
  12.164 +  val is_comb : term -> bool
  12.165 +  val is_abs  : term -> bool
  12.166 +  val is_eq     : term -> bool
  12.167 +  val is_imp    : term -> bool
  12.168 +  val is_forall : term -> bool 
  12.169 +  val is_exists : term -> bool 
  12.170 +  val is_neg    : term -> bool
  12.171 +  val is_conj   : term -> bool
  12.172 +  val is_disj   : term -> bool
  12.173 +  val is_pair   : term -> bool
  12.174 +  val is_pabs   : term -> bool
  12.175  
  12.176 -  (* Construction of a Preterm from a list of Preterms *)
  12.177 -  val list_mk_comb   : (Preterm * Preterm list) -> Preterm
  12.178 -  val list_mk_abs    : (Preterm list * Preterm) -> Preterm
  12.179 -  val list_mk_imp    : (Preterm list * Preterm) -> Preterm
  12.180 -  val list_mk_forall : (Preterm list * Preterm) -> Preterm
  12.181 -  val list_mk_exists : (Preterm list * Preterm) -> Preterm
  12.182 -  val list_mk_conj   : Preterm list -> Preterm
  12.183 -  val list_mk_disj   : Preterm list -> Preterm
  12.184 +  (* Construction of a term from a list of Preterms *)
  12.185 +  val list_mk_abs    : (term list * term) -> term
  12.186 +  val list_mk_imp    : (term list * term) -> term
  12.187 +  val list_mk_forall : (term list * term) -> term
  12.188 +  val list_mk_exists : (term list * term) -> term
  12.189 +  val list_mk_conj   : term list -> term
  12.190 +  val list_mk_disj   : term list -> term
  12.191  
  12.192 -  (* Destructing a Preterm to a list of Preterms *)
  12.193 -  val strip_comb     : Preterm -> (Preterm * Preterm list)
  12.194 -  val strip_abs      : Preterm -> (Preterm list * Preterm)
  12.195 -  val strip_imp      : Preterm -> (Preterm list * Preterm)
  12.196 -  val strip_forall   : Preterm -> (Preterm list * Preterm)
  12.197 -  val strip_exists   : Preterm -> (Preterm list * Preterm)
  12.198 -  val strip_conj     : Preterm -> Preterm list
  12.199 -  val strip_disj     : Preterm -> Preterm list
  12.200 -  val strip_pair     : Preterm -> Preterm list
  12.201 +  (* Destructing a term to a list of Preterms *)
  12.202 +  val strip_comb     : term -> (term * term list)
  12.203 +  val strip_abs      : term -> (term list * term)
  12.204 +  val strip_imp      : term -> (term list * term)
  12.205 +  val strip_forall   : term -> (term list * term)
  12.206 +  val strip_exists   : term -> (term list * term)
  12.207 +  val strip_conj     : term -> term list
  12.208 +  val strip_disj     : term -> term list
  12.209 +  val strip_pair     : term -> term list
  12.210  
  12.211    (* Miscellaneous *)
  12.212 -  val mk_vstruct : Type -> Preterm list -> Preterm
  12.213 -  val gen_all    : Preterm -> Preterm
  12.214 -  val find_term  : (Preterm -> bool) -> Preterm -> Preterm
  12.215 -  val find_terms : (Preterm -> bool) -> Preterm -> Preterm list
  12.216 -  val dest_relation : Preterm -> Preterm * Preterm * Preterm
  12.217 -  val is_WFR : Preterm -> bool
  12.218 -  val ARB : Type -> Preterm
  12.219 +  val mk_vstruct : typ -> term list -> term
  12.220 +  val gen_all    : term -> term
  12.221 +  val find_term  : (term -> bool) -> term -> term
  12.222 +  val find_terms : (term -> bool) -> term -> term list
  12.223 +  val dest_relation : term -> term * term * term
  12.224 +  val is_WFR : term -> bool
  12.225 +  val ARB : typ -> term
  12.226  
  12.227    (* Prettyprinting *)
  12.228 -  val Term_to_string : Term -> string
  12.229 +  val Term_to_string : cterm -> string
  12.230  end;
    13.1 --- a/TFL/usyntax.sml	Tue May 20 11:47:33 1997 +0200
    13.2 +++ b/TFL/usyntax.sml	Tue May 20 11:49:57 1997 +0200
    13.3 @@ -10,24 +10,15 @@
    13.4  
    13.5  fun ERR{func,mesg} = Utils.ERR{module = "USyntax", func = func, mesg = mesg};
    13.6  
    13.7 -type Type = typ
    13.8 -type Term = cterm
    13.9 -type Preterm = term
   13.10 -
   13.11  
   13.12  (*---------------------------------------------------------------------------
   13.13   *
   13.14   *                            Types 
   13.15   *
   13.16   *---------------------------------------------------------------------------*)
   13.17 -fun mk_type{Tyop, Args} = Type(Tyop,Args);
   13.18  val mk_prim_vartype = TVar;
   13.19  fun mk_vartype s = mk_prim_vartype((s,0),["term"]);
   13.20  
   13.21 -fun dest_type(Type(ty,args)) = {Tyop = ty, Args = args}
   13.22 -  | dest_type _ = raise ERR{func = "dest_type", mesg = "Not a compound type"};
   13.23 -
   13.24 -
   13.25  (* But internally, it's useful *)
   13.26  fun dest_vtype (TVar x) = x
   13.27    | dest_vtype _ = raise ERR{func = "dest_vtype", 
   13.28 @@ -36,14 +27,12 @@
   13.29  val is_vartype = Utils.can dest_vtype;
   13.30  
   13.31  val type_vars  = map mk_prim_vartype o typ_tvars
   13.32 -fun type_varsl L = Utils.mk_set (Utils.curry op=)
   13.33 -                      (Utils.rev_itlist (Utils.curry op @ o type_vars) L []);
   13.34 +fun type_varsl L = Utils.mk_set (curry op=)
   13.35 +                      (Utils.rev_itlist (curry op @ o type_vars) L []);
   13.36  
   13.37  val alpha  = mk_vartype "'a"
   13.38  val beta   = mk_vartype "'b"
   13.39  
   13.40 -val bool = Type("bool",[]);
   13.41 -
   13.42  fun match_type ty1 ty2 = raise ERR{func="match_type",mesg="not implemented"};
   13.43  
   13.44  
   13.45 @@ -52,19 +41,11 @@
   13.46  val --> = -->;
   13.47  infixr 3 -->;
   13.48  
   13.49 -(* hol_type -> hol_type list * hol_type *)
   13.50 -fun strip_type ty =
   13.51 -   let val {Tyop = "fun", Args = [ty1,ty2]} = dest_type ty
   13.52 -       val (D,r) = strip_type ty2
   13.53 -   in (ty1::D, r)
   13.54 -   end
   13.55 -   handle _ => ([],ty);
   13.56 +fun strip_type ty = (binder_types ty, body_type ty);
   13.57  
   13.58 -(* hol_type -> hol_type list *)
   13.59 -fun strip_prod_type ty =
   13.60 -   let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty
   13.61 -   in strip_prod_type ty1 @ strip_prod_type ty2
   13.62 -   end handle _ => [ty];
   13.63 +fun strip_prod_type (Type("*", [ty1,ty2])) =
   13.64 +	strip_prod_type ty1 @ strip_prod_type ty2
   13.65 +  | strip_prod_type ty = [ty];
   13.66  
   13.67  
   13.68  
   13.69 @@ -74,7 +55,7 @@
   13.70   *
   13.71   *---------------------------------------------------------------------------*)
   13.72  nonfix aconv;
   13.73 -val aconv = Utils.curry (op aconv);
   13.74 +val aconv = curry (op aconv);
   13.75  
   13.76  fun free_vars tm = add_term_frees(tm,[]);
   13.77  
   13.78 @@ -94,9 +75,8 @@
   13.79  
   13.80  
   13.81  fun free_varsl L = Utils.mk_set aconv
   13.82 -                      (Utils.rev_itlist (Utils.curry op @ o free_vars) L []);
   13.83 +                      (Utils.rev_itlist (curry op @ o free_vars) L []);
   13.84  
   13.85 -val type_of =  type_of;
   13.86  val type_vars_in_term = map mk_prim_vartype o term_tvars;
   13.87  
   13.88  (* Can't really be very exact in Isabelle *)
   13.89 @@ -110,7 +90,7 @@
   13.90    in rev(add(tm,[]))
   13.91    end;
   13.92  fun all_varsl L = Utils.mk_set aconv
   13.93 -                      (Utils.rev_itlist (Utils.curry op @ o all_vars) L []);
   13.94 +                      (Utils.rev_itlist (curry op @ o all_vars) L []);
   13.95  
   13.96  
   13.97  (* Prelogic *)
   13.98 @@ -151,52 +131,42 @@
   13.99    | mk_abs{Bvar as Free(s,ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
  13.100    | mk_abs _ = raise ERR{func = "mk_abs", mesg = "Bvar is not a variable"};
  13.101  
  13.102 -fun list_mk_comb (h,[]) = h
  13.103 -  | list_mk_comb (h,L) =
  13.104 -      rev_itlist (fn t1 => fn t2 => mk_comb{Rator = t2, Rand = t1}) L h;
  13.105 -
  13.106 -
  13.107 -fun mk_eq{lhs,rhs} = 
  13.108 -   let val ty = type_of lhs
  13.109 -       val c = mk_const{Name = "op =", Ty = ty --> ty --> bool}
  13.110 -   in list_mk_comb(c,[lhs,rhs])
  13.111 -   end
  13.112  
  13.113  fun mk_imp{ant,conseq} = 
  13.114 -   let val c = mk_const{Name = "op -->", Ty = bool --> bool --> bool}
  13.115 -   in list_mk_comb(c,[ant,conseq])
  13.116 +   let val c = mk_const{Name = "op -->", Ty = HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT}
  13.117 +   in list_comb(c,[ant,conseq])
  13.118     end;
  13.119  
  13.120  fun mk_select (r as {Bvar,Body}) = 
  13.121    let val ty = type_of Bvar
  13.122 -      val c = mk_const{Name = "Eps", Ty = (ty --> bool) --> ty}
  13.123 -  in list_mk_comb(c,[mk_abs r])
  13.124 +      val c = mk_const{Name = "Eps", Ty = (ty --> HOLogic.boolT) --> ty}
  13.125 +  in list_comb(c,[mk_abs r])
  13.126    end;
  13.127  
  13.128  fun mk_forall (r as {Bvar,Body}) = 
  13.129    let val ty = type_of Bvar
  13.130 -      val c = mk_const{Name = "All", Ty = (ty --> bool) --> bool}
  13.131 -  in list_mk_comb(c,[mk_abs r])
  13.132 +      val c = mk_const{Name = "All", Ty = (ty --> HOLogic.boolT) --> HOLogic.boolT}
  13.133 +  in list_comb(c,[mk_abs r])
  13.134    end;
  13.135  
  13.136  fun mk_exists (r as {Bvar,Body}) = 
  13.137    let val ty = type_of Bvar 
  13.138 -      val c = mk_const{Name = "Ex", Ty = (ty --> bool) --> bool}
  13.139 -  in list_mk_comb(c,[mk_abs r])
  13.140 +      val c = mk_const{Name = "Ex", Ty = (ty --> HOLogic.boolT) --> HOLogic.boolT}
  13.141 +  in list_comb(c,[mk_abs r])
  13.142    end;
  13.143  
  13.144  
  13.145  fun mk_conj{conj1,conj2} =
  13.146 -   let val c = mk_const{Name = "op &", Ty = bool --> bool --> bool}
  13.147 -   in list_mk_comb(c,[conj1,conj2])
  13.148 +   let val c = mk_const{Name = "op &", Ty = HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT}
  13.149 +   in list_comb(c,[conj1,conj2])
  13.150     end;
  13.151  
  13.152  fun mk_disj{disj1,disj2} =
  13.153 -   let val c = mk_const{Name = "op |", Ty = bool --> bool --> bool}
  13.154 -   in list_mk_comb(c,[disj1,disj2])
  13.155 +   let val c = mk_const{Name = "op |", Ty = HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT}
  13.156 +   in list_comb(c,[disj1,disj2])
  13.157     end;
  13.158  
  13.159 -fun prod_ty ty1 ty2 = mk_type{Tyop = "*", Args = [ty1,ty2]};
  13.160 +fun prod_ty ty1 ty2 = Type("*", [ty1,ty2]);
  13.161  
  13.162  local
  13.163  fun mk_uncurry(xt,yt,zt) =
  13.164 @@ -220,10 +190,10 @@
  13.165  
  13.166  (* Destruction routines *)
  13.167  
  13.168 -datatype lambda = VAR   of {Name : string, Ty : Type}
  13.169 -                | CONST of {Name : string, Ty : Type}
  13.170 -                | COMB  of {Rator: Preterm, Rand : Preterm}
  13.171 -                | LAMB  of {Bvar : Preterm, Body : Preterm};
  13.172 +datatype lambda = VAR   of {Name : string, Ty : typ}
  13.173 +                | CONST of {Name : string, Ty : typ}
  13.174 +                | COMB  of {Rator: term, Rand : term}
  13.175 +                | LAMB  of {Bvar : term, Body : term};
  13.176  
  13.177  
  13.178  fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty}
  13.179 @@ -279,25 +249,27 @@
  13.180     let val ty1 = type_of fst
  13.181         val ty2 = type_of snd
  13.182         val c = mk_const{Name = "Pair", Ty = ty1 --> ty2 --> prod_ty ty1 ty2}
  13.183 -   in list_mk_comb(c,[fst,snd])
  13.184 +   in list_comb(c,[fst,snd])
  13.185     end;
  13.186  
  13.187  fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
  13.188    | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"};
  13.189  
  13.190  
  13.191 -local  val ucheck = Utils.assert (curry (op =) "split" o #Name o dest_const)
  13.192 +local  fun ucheck t = (if #Name(dest_const t) = "split" then t
  13.193 +                       else raise Match)
  13.194  in
  13.195  fun dest_pabs tm =
  13.196     let val {Bvar,Body} = dest_abs tm
  13.197     in {varstruct = Bvar, body = Body}
  13.198 -   end handle _ 
  13.199 -   => let val {Rator,Rand} = dest_comb tm
  13.200 -          val _ = ucheck Rator
  13.201 -          val {varstruct = lv,body} = dest_pabs Rand
  13.202 -          val {varstruct = rv,body} = dest_pabs body
  13.203 -      in {varstruct = mk_pair{fst = lv, snd = rv}, body = body}
  13.204 -      end
  13.205 +   end 
  13.206 +    handle 
  13.207 +     _ => let val {Rator,Rand} = dest_comb tm
  13.208 +              val _ = ucheck Rator
  13.209 +              val {varstruct = lv,body} = dest_pabs Rand
  13.210 +              val {varstruct = rv,body} = dest_pabs body
  13.211 +          in {varstruct = mk_pair{fst = lv, snd = rv}, body = body}
  13.212 +          end
  13.213  end;
  13.214  
  13.215  
  13.216 @@ -326,7 +298,7 @@
  13.217  val is_pabs   = can dest_pabs
  13.218  
  13.219  
  13.220 -(* Construction of a Term from a list of Terms *)
  13.221 +(* Construction of a cterm from a list of Terms *)
  13.222  
  13.223  fun list_mk_abs(L,tm) = itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
  13.224  
  13.225 @@ -341,7 +313,7 @@
  13.226  (* Need to reverse? *)
  13.227  fun gen_all tm = list_mk_forall(free_vars tm, tm);
  13.228  
  13.229 -(* Destructing a Term to a list of Terms *)
  13.230 +(* Destructing a cterm to a list of Terms *)
  13.231  fun strip_comb tm = 
  13.232     let fun dest(M$N, A) = dest(M, N::A)
  13.233           | dest x = x
  13.234 @@ -359,7 +331,7 @@
  13.235  fun strip_imp fm =
  13.236     if (is_imp fm)
  13.237     then let val {ant,conseq} = dest_imp fm
  13.238 -	    val (was,wb) = strip_imp conseq
  13.239 +            val (was,wb) = strip_imp conseq
  13.240          in ((ant::was), wb)
  13.241          end
  13.242     else ([],fm);
  13.243 @@ -411,25 +383,15 @@
  13.244  
  13.245  fun mk_preterm tm = #t(rep_cterm tm);
  13.246  
  13.247 -fun mk_prop (tm as Const("Trueprop",_) $ _) = tm
  13.248 -  | mk_prop tm = mk_comb{Rator=mk_const{Name = "Trueprop", 
  13.249 -                           Ty = bool --> mk_type{Tyop = "prop",Args=[]}},
  13.250 -                         Rand = tm};
  13.251 -
  13.252 -fun drop_Trueprop (Const("Trueprop",_) $ X) = X
  13.253 -  | drop_Trueprop X = X;
  13.254 -
  13.255  (* Miscellaneous *)
  13.256  
  13.257  fun mk_vstruct ty V =
  13.258 -  let fun follow_prod_type ty vs =
  13.259 -      let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty
  13.260 -          val (ltm,vs1) = follow_prod_type ty1 vs
  13.261 -          val (rtm,vs2) = follow_prod_type ty2 vs1
  13.262 -      in (mk_pair{fst=ltm, snd=rtm}, vs2)
  13.263 -      end handle _ => (hd vs, tl vs)
  13.264 - in fst(follow_prod_type ty V)
  13.265 - end;
  13.266 +  let fun follow_prod_type (Type("*",[ty1,ty2])) vs =
  13.267 +	      let val (ltm,vs1) = follow_prod_type ty1 vs
  13.268 +		  val (rtm,vs2) = follow_prod_type ty2 vs1
  13.269 +	      in (mk_pair{fst=ltm, snd=rtm}, vs2) end
  13.270 +	| follow_prod_type _ (v::vs) = (v,vs)
  13.271 +  in #1 (follow_prod_type ty V)  end;
  13.272  
  13.273  
  13.274  (* Search a term for a sub-term satisfying the predicate p. *)
  13.275 @@ -446,7 +408,7 @@
  13.276     end;
  13.277  
  13.278  (*******************************************************************
  13.279 - * find_terms: (term -> bool) -> term -> term list
  13.280 + * find_terms: (term -> HOLogic.boolT) -> term -> term list
  13.281   * 
  13.282   *  Find all subterms in a term that satisfy a given predicate p.
  13.283   *
  13.284 @@ -467,7 +429,7 @@
  13.285  val Term_to_string = string_of_cterm;
  13.286  
  13.287  fun dest_relation tm =
  13.288 -   if (type_of tm = bool)
  13.289 +   if (type_of tm = HOLogic.boolT)
  13.290     then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
  13.291          in (R,y,x)
  13.292          end handle _ => raise ERR{func="dest_relation",
  13.293 @@ -477,6 +439,6 @@
  13.294  fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false;
  13.295  
  13.296  fun ARB ty = mk_select{Bvar=mk_var{Name="v",Ty=ty},
  13.297 -                       Body=mk_const{Name="True",Ty=bool}};
  13.298 +                       Body=mk_const{Name="True",Ty=HOLogic.boolT}};
  13.299  
  13.300  end; (* Syntax *)
    14.1 --- a/TFL/utils.sig	Tue May 20 11:47:33 1997 +0200
    14.2 +++ b/TFL/utils.sig	Tue May 20 11:49:57 1997 +0200
    14.3 @@ -4,50 +4,25 @@
    14.4    exception ERR of {module:string,func:string, mesg:string}
    14.5    val Raise : exn -> 'a
    14.6  
    14.7 -  (* infix 3 ## *)
    14.8 -  val ## : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd
    14.9    val can   : ('a -> 'b) -> 'a -> bool
   14.10    val holds : ('a -> bool) -> 'a -> bool
   14.11 -  val assert: ('a -> bool) -> 'a -> 'a
   14.12 -  val W : ('a -> 'a -> 'b) -> 'a -> 'b
   14.13    val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
   14.14 -  val I : 'a -> 'a
   14.15 -  val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
   14.16 -  val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c
   14.17 -  val fst : 'a * 'b -> 'a
   14.18 -  val snd : 'a * 'b -> 'b
   14.19 -
   14.20 -  (* option type *)
   14.21 -  datatype 'a option = SOME of 'a | NONE
   14.22  
   14.23    (* Set operations *)
   14.24    val mem : ('a -> 'a -> bool) -> 'a -> 'a list -> bool
   14.25 -  val union : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
   14.26 -  val Union : ('a -> 'a -> bool) -> 'a list list ->  'a list
   14.27 -  val intersect : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
   14.28    val set_diff : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list
   14.29    val mk_set : ('a -> 'a -> bool) -> 'a list -> 'a list
   14.30 -  val set_eq : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
   14.31  
   14.32 -  val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   14.33    val itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   14.34    val rev_itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   14.35    val end_itlist : ('a -> 'a -> 'a) -> 'a list -> 'a
   14.36    val itlist2 :('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   14.37 -  val filter : ('a -> bool) -> 'a list -> 'a list
   14.38    val mapfilter : ('a -> 'b) -> 'a list -> 'b list
   14.39    val pluck : ('a -> bool) -> 'a list -> 'a * 'a list
   14.40 -  val assoc1 : ('a*'a->bool) -> 'a -> ('a * 'b) list -> ('a * 'b) option
   14.41    val front_back : 'a list -> 'a list * 'a
   14.42 -  val all : ('a -> bool) -> 'a list -> bool
   14.43 -  val exists : ('a -> bool) -> 'a list -> bool
   14.44 -  val zip : 'a list -> 'b list -> ('a*'b) list
   14.45    val zip3 : 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
   14.46 -  val unzip : ('a*'b) list -> ('a list * 'b list)
   14.47    val take  : ('a -> 'b) -> int * 'a list -> 'b list
   14.48    val sort  : ('a -> 'a -> bool) -> 'a list -> 'a list
   14.49 -
   14.50 -  val int_to_string : int -> string
   14.51    val concat : string -> string -> string
   14.52    val quote : string -> string
   14.53  
    15.1 --- a/TFL/utils.sml	Tue May 20 11:47:33 1997 +0200
    15.2 +++ b/TFL/utils.sml	Tue May 20 11:49:57 1997 +0200
    15.3 @@ -1,10 +1,9 @@
    15.4  (*---------------------------------------------------------------------------
    15.5 - * Some common utilities. This strucuture is parameterized over
    15.6 - * "int_to_string" because there is a difference between the string 
    15.7 - * operations of SML/NJ versions 93 and 109.
    15.8 + * Some common utilities.
    15.9   *---------------------------------------------------------------------------*)
   15.10  
   15.11 -functor UTILS (val int_to_string : int -> string) :Utils_sig = 
   15.12 +
   15.13 +structure Utils = 
   15.14  struct
   15.15  
   15.16  (* Standard exception for TFL. *)
   15.17 @@ -19,40 +18,18 @@
   15.18  val MESG_string = info_string "Message"
   15.19  end;
   15.20  
   15.21 -fun Raise (e as ERR sss) = (output(std_out, ERR_string sss);  raise e)
   15.22 +fun Raise (e as ERR sss) = (TextIO.output(TextIO.stdOut, ERR_string sss);  
   15.23 +                            raise e)
   15.24    | Raise e = raise e;
   15.25  
   15.26  
   15.27 -(* option type *)
   15.28 -datatype 'a option = SOME of 'a | NONE
   15.29 -
   15.30 -
   15.31  (* Simple combinators *)
   15.32  
   15.33 -infix 3 ##
   15.34 -fun f ## g = (fn (x,y) => (f x, g y))
   15.35 -
   15.36 -fun W f x = f x x
   15.37  fun C f x y = f y x
   15.38 -fun I x = x
   15.39 -
   15.40 -fun curry f x y = f(x,y)
   15.41 -fun uncurry f (x,y) = f x y
   15.42 -
   15.43 -fun fst(x,y) = x
   15.44 -fun snd(x,y) = y;
   15.45  
   15.46  val concat = curry (op ^)
   15.47  fun quote s = "\""^s^"\"";
   15.48  
   15.49 -fun map2 f L1 L2 =
   15.50 - let fun mp2 [] [] L = rev L
   15.51 -       | mp2 (a1::rst1) (a2::rst2) L = mp2 rst1 rst2 (f a1 a2::L)
   15.52 -       | mp2 _ _ _ = raise UTILS_ERR{func="map2",mesg="different length lists"}
   15.53 -   in mp2 L1 L2 []
   15.54 -   end;
   15.55 -
   15.56 -
   15.57  fun itlist f L base_value =
   15.58     let fun it [] = base_value
   15.59           | it (a::rst) = f a (it rst)
   15.60 @@ -81,8 +58,6 @@
   15.61   in  it (L1,L2)
   15.62   end;
   15.63  
   15.64 -fun filter p L = itlist (fn x => fn y => if (p x) then x::y else y) L []
   15.65 -
   15.66  fun mapfilter f alist = itlist (fn i=>fn L=> (f i::L) handle _ => L) alist [];
   15.67  
   15.68  fun pluck p  =
   15.69 @@ -104,24 +79,6 @@
   15.70    in grab
   15.71    end;
   15.72  
   15.73 -fun all p =
   15.74 -   let fun every [] = true
   15.75 -         | every (a::rst) = (p a) andalso every rst       
   15.76 -   in every 
   15.77 -   end;
   15.78 -
   15.79 -fun exists p =
   15.80 -   let fun ex [] = false
   15.81 -         | ex (a::rst) = (p a) orelse ex rst       
   15.82 -   in ex 
   15.83 -   end;
   15.84 -
   15.85 -fun zip [] [] = []
   15.86 -  | zip (a::b) (c::d) = (a,c)::(zip b d)
   15.87 -  | zip _ _ = raise UTILS_ERR{func = "zip",mesg = "different length lists"};
   15.88 -
   15.89 -fun unzip L = itlist (fn (x,y) => fn (l1,l2) =>((x::l1),(y::l2))) L ([],[]);
   15.90 -
   15.91  fun zip3 [][][] = []
   15.92    | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3
   15.93    | zip3 _ _ _ = raise UTILS_ERR{func="zip3",mesg="different lengths"};
   15.94 @@ -131,18 +88,8 @@
   15.95  fun holds P x = P x handle _ => false;
   15.96  
   15.97  
   15.98 -fun assert p x = 
   15.99 - if (p x) then x else raise UTILS_ERR{func="assert", mesg="predicate not true"}
  15.100 -
  15.101 -fun assoc1 eq item =
  15.102 -   let fun assc ((entry as (key,_))::rst) = 
  15.103 -             if eq(item,key) then SOME entry else assc rst
  15.104 -         | assc [] = NONE
  15.105 -    in assc
  15.106 -    end;
  15.107 -
  15.108  (* Set ops *)
  15.109 -nonfix mem union;  (* Gag Barf Choke *)
  15.110 +nonfix mem;  (* Gag Barf Choke *)
  15.111  fun mem eq_func i =
  15.112     let val eqi = eq_func i
  15.113         fun mm [] = false
  15.114 @@ -150,14 +97,6 @@
  15.115     in mm
  15.116     end;
  15.117  
  15.118 -fun union eq_func =
  15.119 -   let val mem = mem eq_func
  15.120 -       fun un S1 []  = S1
  15.121 -         | un [] S1  = S1
  15.122 -         | un (a::rst) S2 = if (mem a S2) then (un rst S2) else (a::un rst S2)
  15.123 -   in un
  15.124 -   end;
  15.125 -
  15.126  fun mk_set eq_func =
  15.127     let val mem = mem eq_func
  15.128         fun mk [] = []
  15.129 @@ -165,17 +104,9 @@
  15.130     in mk
  15.131     end;
  15.132  
  15.133 -(* Union of a family of sets *)
  15.134 -fun Union eq_func set_o_sets = itlist (union eq_func) set_o_sets [];
  15.135 -
  15.136 -fun intersect eq_func S1 S2 = mk_set eq_func (filter (C (mem eq_func) S2) S1);
  15.137 -
  15.138  (* All the elements in the first set that are not also in the second set. *)
  15.139  fun set_diff eq_func S1 S2 = filter (fn x => not (mem eq_func x S2)) S1
  15.140  
  15.141 -fun set_eq eq_func S1 S2 = 
  15.142 -   null(set_diff eq_func S1 S2) andalso null(set_diff eq_func S2 S1);
  15.143 -
  15.144  
  15.145  fun sort R = 
  15.146  let fun part (m, []) = ([],[])
  15.147 @@ -192,6 +123,5 @@
  15.148  end;
  15.149  
  15.150  
  15.151 -val int_to_string = int_to_string;
  15.152  
  15.153  end; (* Utils *)