Removal of module Mask and datatype binding with its constructor |->
authorpaulson
Tue May 27 13:22:30 1997 +0200 (1997-05-27)
changeset 33539112a2efb9a3
parent 3352 04502e5431fb
child 3354 3dac85693547
Removal of module Mask and datatype binding with its constructor |->
TFL/mask.sig
TFL/mask.sml
TFL/rules.new.sml
TFL/rules.sig
TFL/sys.sml
TFL/tfl.sml
TFL/thry.sig
TFL/thry.sml
TFL/usyntax.sig
TFL/usyntax.sml
     1.1 --- a/TFL/mask.sig	Tue May 27 13:03:41 1997 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,14 +0,0 @@
     1.4 -(*  Title:      TFL/mask
     1.5 -    ID:         $Id$
     1.6 -    Author:     Konrad Slind, Cambridge University Computer Laboratory
     1.7 -    Copyright   1997  University of Cambridge
     1.8 -*)
     1.9 -
    1.10 -signature Mask_sig =
    1.11 -sig
    1.12 - datatype 'a binding = |-> of ('a * 'a)  (* infix 7 |->; *)
    1.13 -
    1.14 - type mask
    1.15 - val ERR : mask
    1.16 -
    1.17 -end
     2.1 --- a/TFL/mask.sml	Tue May 27 13:03:41 1997 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,22 +0,0 @@
     2.4 -(*  Title:      TFL/mask
     2.5 -    ID:         $Id$
     2.6 -    Author:     Konrad Slind, Cambridge University Computer Laboratory
     2.7 -    Copyright   1997  University of Cambridge
     2.8 -*)
     2.9 -
    2.10 -(*---------------------------------------------------------------------------
    2.11 - * This structure is intended to shield TFL from any constructors already 
    2.12 - * declared in the environment. In the Isabelle port, for example, there
    2.13 - * was already a datatype with "|->" being a constructor. In TFL we were
    2.14 - * trying to define a function "|->", but it failed in PolyML (which conforms
    2.15 - * better to the Standard) while the definition was accepted in NJ/SML
    2.16 - * (which doesn't always conform so well to the standard).
    2.17 - *---------------------------------------------------------------------------*)
    2.18 -
    2.19 -structure Mask : Mask_sig =
    2.20 -struct
    2.21 -
    2.22 - datatype 'a binding = |-> of ('a * 'a)   (* infix 7 |->; *)
    2.23 -
    2.24 - datatype mask = ERR 
    2.25 -end;
     3.1 --- a/TFL/rules.new.sml	Tue May 27 13:03:41 1997 +0200
     3.2 +++ b/TFL/rules.new.sml	Tue May 27 13:22:30 1997 +0200
     3.3 @@ -10,8 +10,6 @@
     3.4  struct
     3.5  
     3.6  open Utils;
     3.7 -open Mask;
     3.8 -infix 7 |->;
     3.9  
    3.10  structure USyntax  = USyntax;
    3.11  structure S  = USyntax;
    3.12 @@ -53,7 +51,7 @@
    3.13   *---------------------------------------------------------------------------*)
    3.14  fun INST_TYPE blist thm = 
    3.15    let val {sign,...} = rep_thm thm
    3.16 -      val blist' = map (fn (TVar(idx,_) |-> B) => (idx, ctyp_of sign B)) blist
    3.17 +      val blist' = map (fn (TVar(idx,_), B) => (idx, ctyp_of sign B)) blist
    3.18    in Thm.instantiate (blist',[]) thm
    3.19    end
    3.20    handle _ => raise RULES_ERR{func = "INST_TYPE", mesg = ""};
    3.21 @@ -368,18 +366,19 @@
    3.22   *       A |- ?y_1...y_n. M
    3.23   *
    3.24   *---------------------------------------------------------------------------*)
    3.25 -(* Could be improved, but needs "subst" for certified terms *)
    3.26 +(* Could be improved, but needs "subst_free" for certified terms *)
    3.27  
    3.28  fun IT_EXISTS blist th = 
    3.29     let val {sign,...} = rep_thm th
    3.30         val tych = cterm_of sign
    3.31         val detype = #t o rep_cterm
    3.32 -       val blist' = map (fn (x|->y) => (detype x |-> detype y)) blist
    3.33 +       val blist' = map (fn (x,y) => (detype x, detype y)) blist
    3.34         fun ?v M  = cterm_of sign (S.mk_exists{Bvar=v,Body = M})
    3.35         
    3.36    in
    3.37 -  U.itlist (fn (b as (r1 |-> r2)) => fn thm => 
    3.38 -        EXISTS(?r2(S.subst[b] (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
    3.39 +  U.itlist (fn (b as (r1,r2)) => fn thm => 
    3.40 +        EXISTS(?r2(subst_free[b] 
    3.41 +		   (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
    3.42                thm)
    3.43         blist' th
    3.44    end;
    3.45 @@ -389,10 +388,10 @@
    3.46   * fun IT_EXISTS blist th = 
    3.47   *    let val {sign,...} = rep_thm th
    3.48   *        val tych = cterm_of sign
    3.49 - *        fun detype (x |-> y) = ((#t o rep_cterm) x |-> (#t o rep_cterm) y)
    3.50 + *        fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y)
    3.51   *   in
    3.52 - *  fold (fn (b as (r1|->r2), thm) => 
    3.53 - *  EXISTS(D.mk_exists(r2, tych(S.subst[detype b](#t(rep_cterm(cconcl thm))))),
    3.54 + *  fold (fn (b as (r1,r2), thm) => 
    3.55 + *  EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))),
    3.56   *           r1) thm)  blist th
    3.57   *   end;
    3.58   *---------------------------------------------------------------------------*)
    3.59 @@ -692,9 +691,8 @@
    3.60                                        (ListPair.zip (vlist, args)))
    3.61                                 "assertion failed in CONTEXT_REWRITE_RULE"
    3.62  (*                val fbvs1 = variants (S.free_vars imp) fbvs *)
    3.63 -                  val imp_body1 = S.subst (map (op|->) 
    3.64 -                                           (ListPair.zip (args, vstrl)))
    3.65 -                                          imp_body
    3.66 +                  val imp_body1 = subst_free (ListPair.zip (args, vstrl))
    3.67 +                                             imp_body
    3.68                    val tych = cterm_of sign
    3.69                    val ants1 = map tych (Logic.strip_imp_prems imp_body1)
    3.70                    val eq1 = Logic.strip_imp_concl imp_body1
     4.1 --- a/TFL/rules.sig	Tue May 27 13:03:41 1997 +0200
     4.2 +++ b/TFL/rules.sig	Tue May 27 13:22:30 1997 +0200
     4.3 @@ -9,8 +9,6 @@
     4.4  signature Rules_sig =
     4.5  sig
     4.6  (*  structure USyntax : USyntax_sig *)
     4.7 -  type 'a binding
     4.8 -
     4.9    val dest_thm : thm -> term list * term
    4.10  
    4.11    (* Inference rules *)
    4.12 @@ -23,7 +21,7 @@
    4.13    val CONJUNCTS :thm -> thm list
    4.14    val DISCH     :cterm -> thm -> thm
    4.15    val UNDISCH   :thm  -> thm
    4.16 -  val INST_TYPE :typ binding list -> thm -> thm
    4.17 +  val INST_TYPE :(typ*typ)list -> thm -> thm
    4.18    val SPEC      :cterm -> thm -> thm
    4.19    val ISPEC     :cterm -> thm -> thm
    4.20    val ISPECL    :cterm list -> thm -> thm
    4.21 @@ -42,7 +40,7 @@
    4.22    val CHOOSE : cterm * thm -> thm -> thm
    4.23    val EXISTS : cterm * cterm -> thm -> thm
    4.24    val EXISTL : cterm list -> thm -> thm
    4.25 -  val IT_EXISTS : cterm binding list -> thm -> thm
    4.26 +  val IT_EXISTS : (cterm*cterm) list -> thm -> thm
    4.27  
    4.28    val EVEN_ORS : thm list -> thm list
    4.29    val DISJ_CASESL : thm -> thm list -> thm
     5.1 --- a/TFL/sys.sml	Tue May 27 13:03:41 1997 +0200
     5.2 +++ b/TFL/sys.sml	Tue May 27 13:22:30 1997 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      TFL/mask
     5.5 +(*  Title:      TFL/sys
     5.6      ID:         $Id$
     5.7      Author:     Konrad Slind, Cambridge University Computer Laboratory
     5.8      Copyright   1997  University of Cambridge
     5.9 @@ -8,8 +8,6 @@
    5.10  
    5.11  (* Portability stuff *)
    5.12  nonfix prefix;
    5.13 -use"mask.sig";
    5.14 -use"mask.sml";
    5.15  
    5.16  (* Establish a base of common and/or helpful functions. *)
    5.17  use "utils.sig";
     6.1 --- a/TFL/tfl.sml	Tue May 27 13:03:41 1997 +0200
     6.2 +++ b/TFL/tfl.sml	Tue May 27 13:22:30 1997 +0200
     6.3 @@ -8,9 +8,7 @@
     6.4  
     6.5  functor TFL(structure Rules : Rules_sig
     6.6              structure Thry  : Thry_sig
     6.7 -            structure Thms  : Thms_sig
     6.8 -            sharing type Rules.binding = Thry.binding = 
     6.9 -                         Thry.USyntax.binding = Mask.binding) : TFL_sig  =
    6.10 +            structure Thms  : Thms_sig) : TFL_sig  =
    6.11  struct
    6.12  
    6.13  (* Declarations *)
    6.14 @@ -25,14 +23,10 @@
    6.15  structure S = USyntax;
    6.16  structure U = S.Utils;
    6.17  
    6.18 -(* Declares 'a binding datatype *)
    6.19 -open Mask;
    6.20 -
    6.21 -nonfix mem --> |->;
    6.22 +nonfix mem -->;
    6.23  val --> = S.-->;
    6.24  
    6.25  infixr 3 -->;
    6.26 -infixr 7 |->;
    6.27  
    6.28  val concl = #2 o R.dest_thm;
    6.29  val hyp = #1 o R.dest_thm;
    6.30 @@ -118,8 +112,8 @@
    6.31  datatype pattern = GIVEN   of term * int
    6.32                   | OMITTED of term * int
    6.33  
    6.34 -fun psubst theta (GIVEN (tm,i)) = GIVEN(S.subst theta tm, i)
    6.35 -  | psubst theta (OMITTED (tm,i)) = OMITTED(S.subst theta tm, i);
    6.36 +fun psubst theta (GIVEN (tm,i)) = GIVEN(subst_free theta tm, i)
    6.37 +  | psubst theta (OMITTED (tm,i)) = OMITTED(subst_free theta tm, i);
    6.38  
    6.39  fun dest_pattern (GIVEN (tm,i)) = ((GIVEN,i),tm)
    6.40    | dest_pattern (OMITTED (tm,i)) = ((OMITTED,i),tm);
    6.41 @@ -217,7 +211,7 @@
    6.42         then let val fresh = fresh_constr ty_match ty fresh_var
    6.43                  fun expnd (c,gvs) = 
    6.44                    let val capp = list_comb(c,gvs)
    6.45 -                  in ((prefix, capp::rst), psubst[p |-> capp] rhs)
    6.46 +                  in ((prefix, capp::rst), psubst[(p,capp)] rhs)
    6.47                    end
    6.48              in map expnd (map fresh constructors)  end
    6.49         else [row]
    6.50 @@ -235,7 +229,7 @@
    6.51           val col0 = map(hd o #2) pat_rectangle
    6.52       in 
    6.53       if (forall is_Free col0) 
    6.54 -     then let val rights' = map (fn(v,e) => psubst[v|->u] e)
    6.55 +     then let val rights' = map (fn(v,e) => psubst[(v,u)] e)
    6.56                                  (ListPair.zip (col0, rights))
    6.57                val pat_rectangle' = map v_to_prefix pat_rectangle
    6.58                val (pref_patl,tm) = mk{path = rstp,
    6.59 @@ -330,7 +324,7 @@
    6.60               of [] => ()
    6.61            | L => mk_functional_err("The following rows (counting from zero)\
    6.62                                     \ are inaccessible: "^stringize L)
    6.63 -     val case_tm' = S.subst [f |-> fvar] case_tm
    6.64 +     val case_tm' = subst_free [(f,fvar)] case_tm
    6.65   in {functional = S.list_mk_abs ([fvar,a], case_tm'),
    6.66       pats = patts2}
    6.67  end end;
    6.68 @@ -497,7 +491,7 @@
    6.69       val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
    6.70       val R'abs = S.rand R'
    6.71       val (def,theory) = Thry.make_definition thy (Name ^ "_def") 
    6.72 -                                                 (S.subst[R1 |-> R'] proto_def)
    6.73 +                                               (subst_free[(R1,R')] proto_def)
    6.74       val fconst = #lhs(S.dest_eq(concl def)) 
    6.75       val tych = Thry.typecheck theory
    6.76       val baz = R.DISCH (tych proto_def)
    6.77 @@ -571,7 +565,7 @@
    6.78   let 
    6.79   val divide = ipartition (gvvariant FV)
    6.80   val tych = Thry.typecheck thy
    6.81 - fun tych_binding(x|->y) = (tych x |-> tych y)
    6.82 + fun tych_binding(x,y) = (tych x, tych y)
    6.83   fun fail s = raise TFL_ERR{func = "mk_case", mesg = s}
    6.84   fun mk{rows=[],...} = fail"no rows"
    6.85     | mk{path=[], rows = [([], (thm, bindings))]} = 
    6.86 @@ -582,7 +576,7 @@
    6.87           val pat_rectangle' = map tl pat_rectangle
    6.88       in 
    6.89       if (forall is_Free col0) (* column 0 is all variables *)
    6.90 -     then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[u|->v]))
    6.91 +     then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)]))
    6.92                                  (ListPair.zip (rights, col0))
    6.93            in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}
    6.94            end
     7.1 --- a/TFL/thry.sig	Tue May 27 13:03:41 1997 +0200
     7.2 +++ b/TFL/thry.sig	Tue May 27 13:22:30 1997 +0200
     7.3 @@ -6,13 +6,11 @@
     7.4  
     7.5  signature Thry_sig =
     7.6  sig
     7.7 -  type 'a binding
     7.8 -
     7.9    structure USyntax : USyntax_sig
    7.10    val match_term : theory -> term -> term 
    7.11 -                    -> term binding list * typ binding list
    7.12 +                    -> (term*term)list * (typ*typ)list
    7.13  
    7.14 -  val match_type : theory -> typ -> typ -> typ binding list
    7.15 +  val match_type : theory -> typ -> typ -> (typ*typ)list
    7.16  
    7.17    val typecheck : theory -> term -> cterm
    7.18  
     8.1 --- a/TFL/thry.sml	Tue May 27 13:03:41 1997 +0200
     8.2 +++ b/TFL/thry.sml	Tue May 27 13:22:30 1997 +0200
     8.3 @@ -8,21 +8,16 @@
     8.4  struct
     8.5  
     8.6  structure USyntax  = USyntax;
     8.7 -
     8.8 -open Mask;
     8.9  structure S = USyntax;
    8.10  
    8.11 -
    8.12  fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
    8.13  
    8.14  (*---------------------------------------------------------------------------
    8.15   *    Matching 
    8.16   *---------------------------------------------------------------------------*)
    8.17  
    8.18 -local open Utils
    8.19 -      infix 3 |->
    8.20 -      fun tybind (x,y) = TVar (x,["term"])  |-> y
    8.21 -      fun tmbind (x,y) = Var  (x,type_of y) |-> y
    8.22 +local fun tybind (x,y) = (TVar (x,["term"]) , y)
    8.23 +      fun tmbind (x,y) = (Var  (x,type_of y), y)
    8.24  in
    8.25   fun match_term thry pat ob = 
    8.26      let val tsig = #tsig(Sign.rep_sg(sign_of thry))
     9.1 --- a/TFL/usyntax.sig	Tue May 27 13:03:41 1997 +0200
     9.2 +++ b/TFL/usyntax.sig	Tue May 27 13:22:30 1997 +0200
     9.3 @@ -10,8 +10,6 @@
     9.4  sig
     9.5    structure Utils : Utils_sig
     9.6  
     9.7 -  type 'a binding
     9.8 -
     9.9    datatype lambda = VAR   of {Name : string, Ty : typ}
    9.10                    | CONST of {Name : string, Ty : typ}
    9.11                    | COMB  of {Rator: term, Rand : term}
    9.12 @@ -28,7 +26,6 @@
    9.13    val -->        : typ * typ -> typ
    9.14    val strip_type : typ -> typ list * typ
    9.15    val strip_prod_type : typ -> typ list
    9.16 -  val match_type: typ -> typ -> typ binding list
    9.17  
    9.18    (* Terms *)
    9.19    val free_vars  : term -> term list
    9.20 @@ -42,8 +39,7 @@
    9.21    
    9.22    (* Prelogic *)
    9.23    val aconv     : term -> term -> bool
    9.24 -  val subst     : term binding list -> term -> term
    9.25 -  val inst      : typ binding list -> term -> term
    9.26 +  val inst      : (typ*typ) list -> term -> term
    9.27    val beta_conv : term -> term
    9.28  
    9.29    (* Construction routines *)
    10.1 --- a/TFL/usyntax.sml	Tue May 27 13:03:41 1997 +0200
    10.2 +++ b/TFL/usyntax.sml	Tue May 27 13:22:30 1997 +0200
    10.3 @@ -11,12 +11,10 @@
    10.4  
    10.5  structure Utils = Utils;
    10.6  open Utils;
    10.7 -open Mask;
    10.8  
    10.9 -infix 7 |->;
   10.10  infix 4 ##;
   10.11  
   10.12 -fun ERR{func,mesg} = Utils.ERR{module = "USyntax", func = func, mesg = mesg};
   10.13 +fun USYN_ERR{func,mesg} = Utils.ERR{module = "USyntax", func = func, mesg = mesg};
   10.14  
   10.15  
   10.16  (*---------------------------------------------------------------------------
   10.17 @@ -29,7 +27,7 @@
   10.18  
   10.19  (* But internally, it's useful *)
   10.20  fun dest_vtype (TVar x) = x
   10.21 -  | dest_vtype _ = raise ERR{func = "dest_vtype", 
   10.22 +  | dest_vtype _ = raise USYN_ERR{func = "dest_vtype", 
   10.23                               mesg = "not a flexible type variable"};
   10.24  
   10.25  val is_vartype = Utils.can dest_vtype;
   10.26 @@ -41,7 +39,6 @@
   10.27  val alpha  = mk_vartype "'a"
   10.28  val beta   = mk_vartype "'b"
   10.29  
   10.30 -fun match_type ty1 ty2 = raise ERR{func="match_type",mesg="not implemented"};
   10.31  
   10.32  
   10.33  (* What nonsense *)
   10.34 @@ -102,13 +99,11 @@
   10.35  
   10.36  
   10.37  (* Prelogic *)
   10.38 -val subst = subst_free o map (fn (a |-> b) => (a,b));
   10.39 -
   10.40 -fun dest_tybinding (v |-> ty) = (#1(dest_vtype v),ty)
   10.41 +fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)
   10.42  fun inst theta = subst_vars (map dest_tybinding theta,[])
   10.43  
   10.44  fun beta_conv((t1 as Abs _ ) $ t2) = betapply(t1,t2)
   10.45 -  | beta_conv _ = raise ERR{func = "beta_conv", mesg = "Not a beta-redex"};
   10.46 +  | beta_conv _ = raise USYN_ERR{func = "beta_conv", mesg = "Not a beta-redex"};
   10.47  
   10.48  
   10.49  (* Construction routines *)
   10.50 @@ -119,7 +114,7 @@
   10.51  
   10.52  local fun var_name(Var((Name,_),_)) = Name
   10.53          | var_name(Free(s,_)) = s
   10.54 -        | var_name _ = raise ERR{func = "variant",
   10.55 +        | var_name _ = raise USYN_ERR{func = "variant",
   10.56                                   mesg = "list elem. is not a variable"}
   10.57  in
   10.58  fun variant [] v = v
   10.59 @@ -127,7 +122,7 @@
   10.60         Var((string_variant (map var_name vlist) Name,i),ty)
   10.61    | variant vlist (Free(Name,ty)) =
   10.62         Free(string_variant (map var_name vlist) Name,ty)
   10.63 -  | variant _ _ = raise ERR{func = "variant",
   10.64 +  | variant _ _ = raise USYN_ERR{func = "variant",
   10.65                              mesg = "2nd arg. should be a variable"}
   10.66  end;
   10.67  
   10.68 @@ -136,7 +131,7 @@
   10.69  
   10.70  fun mk_abs{Bvar as Var((s,_),ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
   10.71    | mk_abs{Bvar as Free(s,ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
   10.72 -  | mk_abs _ = raise ERR{func = "mk_abs", mesg = "Bvar is not a variable"};
   10.73 +  | mk_abs _ = raise USYN_ERR{func = "mk_abs", mesg = "Bvar is not a variable"};
   10.74  
   10.75  
   10.76  fun mk_imp{ant,conseq} = 
   10.77 @@ -179,7 +174,7 @@
   10.78  fun mk_uncurry(xt,yt,zt) =
   10.79      mk_const{Name = "split", Ty = (xt --> yt --> zt) --> prod_ty xt yt --> zt}
   10.80  fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
   10.81 -  | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"}
   10.82 +  | dest_pair _ = raise USYN_ERR{func = "dest_pair", mesg = "not a pair"}
   10.83  fun is_var(Var(_)) = true | is_var (Free _) = true | is_var _ = false
   10.84  in
   10.85  fun mk_pabs{varstruct,body} = 
   10.86 @@ -192,7 +187,7 @@
   10.87              end
   10.88   in mpa(varstruct,body)
   10.89   end
   10.90 - handle _ => raise ERR{func = "mk_pabs", mesg = ""};
   10.91 + handle _ => raise USYN_ERR{func = "mk_pabs", mesg = ""};
   10.92  end;
   10.93  
   10.94  (* Destruction routines *)
   10.95 @@ -210,43 +205,43 @@
   10.96    | dest_term(Abs(s,ty,M))   = let  val v = mk_var{Name = s, Ty = ty}
   10.97                                 in LAMB{Bvar = v, Body = betapply (M,v)}
   10.98                                 end
   10.99 -  | dest_term(Bound _)       = raise ERR{func = "dest_term",mesg = "Bound"};
  10.100 +  | dest_term(Bound _)       = raise USYN_ERR{func = "dest_term",mesg = "Bound"};
  10.101  
  10.102  fun dest_const(Const(s,ty)) = {Name = s, Ty = ty}
  10.103 -  | dest_const _ = raise ERR{func = "dest_const", mesg = "not a constant"};
  10.104 +  | dest_const _ = raise USYN_ERR{func = "dest_const", mesg = "not a constant"};
  10.105  
  10.106  fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
  10.107 -  | dest_comb _ =  raise ERR{func = "dest_comb", mesg = "not a comb"};
  10.108 +  | dest_comb _ =  raise USYN_ERR{func = "dest_comb", mesg = "not a comb"};
  10.109  
  10.110  fun dest_abs(a as Abs(s,ty,M)) = 
  10.111       let val v = mk_var{Name = s, Ty = ty}
  10.112       in {Bvar = v, Body = betapply (a,v)}
  10.113       end
  10.114 -  | dest_abs _ =  raise ERR{func = "dest_abs", mesg = "not an abstraction"};
  10.115 +  | dest_abs _ =  raise USYN_ERR{func = "dest_abs", mesg = "not an abstraction"};
  10.116  
  10.117  fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
  10.118 -  | dest_eq _ = raise ERR{func = "dest_eq", mesg = "not an equality"};
  10.119 +  | dest_eq _ = raise USYN_ERR{func = "dest_eq", mesg = "not an equality"};
  10.120  
  10.121  fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
  10.122 -  | dest_imp _ = raise ERR{func = "dest_imp", mesg = "not an implication"};
  10.123 +  | dest_imp _ = raise USYN_ERR{func = "dest_imp", mesg = "not an implication"};
  10.124  
  10.125  fun dest_select(Const("Eps",_) $ (a as Abs _)) = dest_abs a
  10.126 -  | dest_select _ = raise ERR{func = "dest_select", mesg = "not a select"};
  10.127 +  | dest_select _ = raise USYN_ERR{func = "dest_select", mesg = "not a select"};
  10.128  
  10.129  fun dest_forall(Const("All",_) $ (a as Abs _)) = dest_abs a
  10.130 -  | dest_forall _ = raise ERR{func = "dest_forall", mesg = "not a forall"};
  10.131 +  | dest_forall _ = raise USYN_ERR{func = "dest_forall", mesg = "not a forall"};
  10.132  
  10.133  fun dest_exists(Const("Ex",_) $ (a as Abs _)) = dest_abs a
  10.134 -  | dest_exists _ = raise ERR{func = "dest_exists", mesg="not an existential"};
  10.135 +  | dest_exists _ = raise USYN_ERR{func = "dest_exists", mesg="not an existential"};
  10.136  
  10.137  fun dest_neg(Const("not",_) $ M) = M
  10.138 -  | dest_neg _ = raise ERR{func = "dest_neg", mesg = "not a negation"};
  10.139 +  | dest_neg _ = raise USYN_ERR{func = "dest_neg", mesg = "not a negation"};
  10.140  
  10.141  fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N}
  10.142 -  | dest_conj _ = raise ERR{func = "dest_conj", mesg = "not a conjunction"};
  10.143 +  | dest_conj _ = raise USYN_ERR{func = "dest_conj", mesg = "not a conjunction"};
  10.144  
  10.145  fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N}
  10.146 -  | dest_disj _ = raise ERR{func = "dest_disj", mesg = "not a disjunction"};
  10.147 +  | dest_disj _ = raise USYN_ERR{func = "dest_disj", mesg = "not a disjunction"};
  10.148  
  10.149  fun mk_pair{fst,snd} = 
  10.150     let val ty1 = type_of fst
  10.151 @@ -256,7 +251,7 @@
  10.152     end;
  10.153  
  10.154  fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
  10.155 -  | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"};
  10.156 +  | dest_pair _ = raise USYN_ERR{func = "dest_pair", mesg = "not a pair"};
  10.157  
  10.158  
  10.159  local  fun ucheck t = (if #Name(dest_const t) = "split" then t
  10.160 @@ -404,7 +399,7 @@
  10.161             then find (#Body(dest_abs tm))
  10.162             else let val {Rator,Rand} = dest_comb tm
  10.163                  in find Rator handle _ => find Rand
  10.164 -                end handle _ => raise ERR{func = "find_term",mesg = ""}
  10.165 +                end handle _ => raise USYN_ERR{func = "find_term",mesg = ""}
  10.166     in find
  10.167     end;
  10.168  
  10.169 @@ -431,9 +426,9 @@
  10.170     if (type_of tm = HOLogic.boolT)
  10.171     then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
  10.172          in (R,y,x)
  10.173 -        end handle _ => raise ERR{func="dest_relation",
  10.174 +        end handle _ => raise USYN_ERR{func="dest_relation",
  10.175                                    mesg="unexpected term structure"}
  10.176 -   else raise ERR{func="dest_relation",mesg="not a boolean term"};
  10.177 +   else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
  10.178  
  10.179  fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false;
  10.180