diff -r 71b760618f30 -r 241838c01caf TFL/usyntax.sml
--- a/TFL/usyntax.sml	Tue May 20 11:47:33 1997 +0200
+++ b/TFL/usyntax.sml	Tue May 20 11:49:57 1997 +0200
@@ -10,24 +10,15 @@
 
 fun ERR{func,mesg} = Utils.ERR{module = "USyntax", func = func, mesg = mesg};
 
-type Type = typ
-type Term = cterm
-type Preterm = term
-
 
 (*---------------------------------------------------------------------------
  *
  *                            Types 
  *
  *---------------------------------------------------------------------------*)
-fun mk_type{Tyop, Args} = Type(Tyop,Args);
 val mk_prim_vartype = TVar;
 fun mk_vartype s = mk_prim_vartype((s,0),["term"]);
 
-fun dest_type(Type(ty,args)) = {Tyop = ty, Args = args}
-  | dest_type _ = raise ERR{func = "dest_type", mesg = "Not a compound type"};
-
-
 (* But internally, it's useful *)
 fun dest_vtype (TVar x) = x
   | dest_vtype _ = raise ERR{func = "dest_vtype", 
@@ -36,14 +27,12 @@
 val is_vartype = Utils.can dest_vtype;
 
 val type_vars  = map mk_prim_vartype o typ_tvars
-fun type_varsl L = Utils.mk_set (Utils.curry op=)
-                      (Utils.rev_itlist (Utils.curry op @ o type_vars) L []);
+fun type_varsl L = Utils.mk_set (curry op=)
+                      (Utils.rev_itlist (curry op @ o type_vars) L []);
 
 val alpha  = mk_vartype "'a"
 val beta   = mk_vartype "'b"
 
-val bool = Type("bool",[]);
-
 fun match_type ty1 ty2 = raise ERR{func="match_type",mesg="not implemented"};
 
 
@@ -52,19 +41,11 @@
 val --> = -->;
 infixr 3 -->;
 
-(* hol_type -> hol_type list * hol_type *)
-fun strip_type ty =
-   let val {Tyop = "fun", Args = [ty1,ty2]} = dest_type ty
-       val (D,r) = strip_type ty2
-   in (ty1::D, r)
-   end
-   handle _ => ([],ty);
+fun strip_type ty = (binder_types ty, body_type ty);
 
-(* hol_type -> hol_type list *)
-fun strip_prod_type ty =
-   let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty
-   in strip_prod_type ty1 @ strip_prod_type ty2
-   end handle _ => [ty];
+fun strip_prod_type (Type("*", [ty1,ty2])) =
+	strip_prod_type ty1 @ strip_prod_type ty2
+  | strip_prod_type ty = [ty];
 
 
 
@@ -74,7 +55,7 @@
  *
  *---------------------------------------------------------------------------*)
 nonfix aconv;
-val aconv = Utils.curry (op aconv);
+val aconv = curry (op aconv);
 
 fun free_vars tm = add_term_frees(tm,[]);
 
@@ -94,9 +75,8 @@
 
 
 fun free_varsl L = Utils.mk_set aconv
-                      (Utils.rev_itlist (Utils.curry op @ o free_vars) L []);
+                      (Utils.rev_itlist (curry op @ o free_vars) L []);
 
-val type_of =  type_of;
 val type_vars_in_term = map mk_prim_vartype o term_tvars;
 
 (* Can't really be very exact in Isabelle *)
@@ -110,7 +90,7 @@
   in rev(add(tm,[]))
   end;
 fun all_varsl L = Utils.mk_set aconv
-                      (Utils.rev_itlist (Utils.curry op @ o all_vars) L []);
+                      (Utils.rev_itlist (curry op @ o all_vars) L []);
 
 
 (* Prelogic *)
@@ -151,52 +131,42 @@
   | mk_abs{Bvar as Free(s,ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
   | mk_abs _ = raise ERR{func = "mk_abs", mesg = "Bvar is not a variable"};
 
-fun list_mk_comb (h,[]) = h
-  | list_mk_comb (h,L) =
-      rev_itlist (fn t1 => fn t2 => mk_comb{Rator = t2, Rand = t1}) L h;
-
-
-fun mk_eq{lhs,rhs} = 
-   let val ty = type_of lhs
-       val c = mk_const{Name = "op =", Ty = ty --> ty --> bool}
-   in list_mk_comb(c,[lhs,rhs])
-   end
 
 fun mk_imp{ant,conseq} = 
-   let val c = mk_const{Name = "op -->", Ty = bool --> bool --> bool}
-   in list_mk_comb(c,[ant,conseq])
+   let val c = mk_const{Name = "op -->", Ty = HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT}
+   in list_comb(c,[ant,conseq])
    end;
 
 fun mk_select (r as {Bvar,Body}) = 
   let val ty = type_of Bvar
-      val c = mk_const{Name = "Eps", Ty = (ty --> bool) --> ty}
-  in list_mk_comb(c,[mk_abs r])
+      val c = mk_const{Name = "Eps", Ty = (ty --> HOLogic.boolT) --> ty}
+  in list_comb(c,[mk_abs r])
   end;
 
 fun mk_forall (r as {Bvar,Body}) = 
   let val ty = type_of Bvar
-      val c = mk_const{Name = "All", Ty = (ty --> bool) --> bool}
-  in list_mk_comb(c,[mk_abs r])
+      val c = mk_const{Name = "All", Ty = (ty --> HOLogic.boolT) --> HOLogic.boolT}
+  in list_comb(c,[mk_abs r])
   end;
 
 fun mk_exists (r as {Bvar,Body}) = 
   let val ty = type_of Bvar 
-      val c = mk_const{Name = "Ex", Ty = (ty --> bool) --> bool}
-  in list_mk_comb(c,[mk_abs r])
+      val c = mk_const{Name = "Ex", Ty = (ty --> HOLogic.boolT) --> HOLogic.boolT}
+  in list_comb(c,[mk_abs r])
   end;
 
 
 fun mk_conj{conj1,conj2} =
-   let val c = mk_const{Name = "op &", Ty = bool --> bool --> bool}
-   in list_mk_comb(c,[conj1,conj2])
+   let val c = mk_const{Name = "op &", Ty = HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT}
+   in list_comb(c,[conj1,conj2])
    end;
 
 fun mk_disj{disj1,disj2} =
-   let val c = mk_const{Name = "op |", Ty = bool --> bool --> bool}
-   in list_mk_comb(c,[disj1,disj2])
+   let val c = mk_const{Name = "op |", Ty = HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT}
+   in list_comb(c,[disj1,disj2])
    end;
 
-fun prod_ty ty1 ty2 = mk_type{Tyop = "*", Args = [ty1,ty2]};
+fun prod_ty ty1 ty2 = Type("*", [ty1,ty2]);
 
 local
 fun mk_uncurry(xt,yt,zt) =
@@ -220,10 +190,10 @@
 
 (* Destruction routines *)
 
-datatype lambda = VAR   of {Name : string, Ty : Type}
-                | CONST of {Name : string, Ty : Type}
-                | COMB  of {Rator: Preterm, Rand : Preterm}
-                | LAMB  of {Bvar : Preterm, Body : Preterm};
+datatype lambda = VAR   of {Name : string, Ty : typ}
+                | CONST of {Name : string, Ty : typ}
+                | COMB  of {Rator: term, Rand : term}
+                | LAMB  of {Bvar : term, Body : term};
 
 
 fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty}
@@ -279,25 +249,27 @@
    let val ty1 = type_of fst
        val ty2 = type_of snd
        val c = mk_const{Name = "Pair", Ty = ty1 --> ty2 --> prod_ty ty1 ty2}
-   in list_mk_comb(c,[fst,snd])
+   in list_comb(c,[fst,snd])
    end;
 
 fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
   | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"};
 
 
-local  val ucheck = Utils.assert (curry (op =) "split" o #Name o dest_const)
+local  fun ucheck t = (if #Name(dest_const t) = "split" then t
+                       else raise Match)
 in
 fun dest_pabs tm =
    let val {Bvar,Body} = dest_abs tm
    in {varstruct = Bvar, body = Body}
-   end handle _ 
-   => let val {Rator,Rand} = dest_comb tm
-          val _ = ucheck Rator
-          val {varstruct = lv,body} = dest_pabs Rand
-          val {varstruct = rv,body} = dest_pabs body
-      in {varstruct = mk_pair{fst = lv, snd = rv}, body = body}
-      end
+   end 
+    handle 
+     _ => let val {Rator,Rand} = dest_comb tm
+              val _ = ucheck Rator
+              val {varstruct = lv,body} = dest_pabs Rand
+              val {varstruct = rv,body} = dest_pabs body
+          in {varstruct = mk_pair{fst = lv, snd = rv}, body = body}
+          end
 end;
 
 
@@ -326,7 +298,7 @@
 val is_pabs   = can dest_pabs
 
 
-(* Construction of a Term from a list of Terms *)
+(* Construction of a cterm from a list of Terms *)
 
 fun list_mk_abs(L,tm) = itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
 
@@ -341,7 +313,7 @@
 (* Need to reverse? *)
 fun gen_all tm = list_mk_forall(free_vars tm, tm);
 
-(* Destructing a Term to a list of Terms *)
+(* Destructing a cterm to a list of Terms *)
 fun strip_comb tm = 
    let fun dest(M$N, A) = dest(M, N::A)
          | dest x = x
@@ -359,7 +331,7 @@
 fun strip_imp fm =
    if (is_imp fm)
    then let val {ant,conseq} = dest_imp fm
-	    val (was,wb) = strip_imp conseq
+            val (was,wb) = strip_imp conseq
         in ((ant::was), wb)
         end
    else ([],fm);
@@ -411,25 +383,15 @@
 
 fun mk_preterm tm = #t(rep_cterm tm);
 
-fun mk_prop (tm as Const("Trueprop",_) $ _) = tm
-  | mk_prop tm = mk_comb{Rator=mk_const{Name = "Trueprop", 
-                           Ty = bool --> mk_type{Tyop = "prop",Args=[]}},
-                         Rand = tm};
-
-fun drop_Trueprop (Const("Trueprop",_) $ X) = X
-  | drop_Trueprop X = X;
-
 (* Miscellaneous *)
 
 fun mk_vstruct ty V =
-  let fun follow_prod_type ty vs =
-      let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty
-          val (ltm,vs1) = follow_prod_type ty1 vs
-          val (rtm,vs2) = follow_prod_type ty2 vs1
-      in (mk_pair{fst=ltm, snd=rtm}, vs2)
-      end handle _ => (hd vs, tl vs)
- in fst(follow_prod_type ty V)
- end;
+  let fun follow_prod_type (Type("*",[ty1,ty2])) vs =
+	      let val (ltm,vs1) = follow_prod_type ty1 vs
+		  val (rtm,vs2) = follow_prod_type ty2 vs1
+	      in (mk_pair{fst=ltm, snd=rtm}, vs2) end
+	| follow_prod_type _ (v::vs) = (v,vs)
+  in #1 (follow_prod_type ty V)  end;
 
 
 (* Search a term for a sub-term satisfying the predicate p. *)
@@ -446,7 +408,7 @@
    end;
 
 (*******************************************************************
- * find_terms: (term -> bool) -> term -> term list
+ * find_terms: (term -> HOLogic.boolT) -> term -> term list
  * 
  *  Find all subterms in a term that satisfy a given predicate p.
  *
@@ -467,7 +429,7 @@
 val Term_to_string = string_of_cterm;
 
 fun dest_relation tm =
-   if (type_of tm = bool)
+   if (type_of tm = HOLogic.boolT)
    then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
         in (R,y,x)
         end handle _ => raise ERR{func="dest_relation",
@@ -477,6 +439,6 @@
 fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false;
 
 fun ARB ty = mk_select{Bvar=mk_var{Name="v",Ty=ty},
-                       Body=mk_const{Name="True",Ty=bool}};
+                       Body=mk_const{Name="True",Ty=HOLogic.boolT}};
 
 end; (* Syntax *)