avoid ML structure aliases (especially single-letter abbreviations);
authorwenzelm
Wed Dec 15 15:11:56 2010 +0100 (2010-12-15)
changeset 411646854e9a40edc
parent 41163 3f21a269780e
child 41170 5645aaee6b38
avoid ML structure aliases (especially single-letter abbreviations);
src/HOL/Import/replay.ML
src/HOL/Tools/TFL/dcterm.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/Tools/eqsubst.ML
     1.1 --- a/src/HOL/Import/replay.ML	Wed Dec 15 15:01:34 2010 +0100
     1.2 +++ b/src/HOL/Import/replay.ML	Wed Dec 15 15:11:56 2010 +0100
     1.3 @@ -2,11 +2,9 @@
     1.4      Author:     Sebastian Skalberg (TU Muenchen)
     1.5  *)
     1.6  
     1.7 -structure Replay =
     1.8 +structure Replay =  (* FIXME proper signature *)
     1.9  struct
    1.10  
    1.11 -structure P = ProofKernel
    1.12 -
    1.13  open ProofKernel
    1.14  open ImportRecorder
    1.15  
    1.16 @@ -17,12 +15,12 @@
    1.17  fun replay_proof int_thms thyname thmname prf thy =
    1.18      let
    1.19          val _ = ImportRecorder.start_replay_proof thyname thmname 
    1.20 -        fun rp (PRefl tm) thy = P.REFL tm thy
    1.21 +        fun rp (PRefl tm) thy = ProofKernel.REFL tm thy
    1.22            | rp (PInstT(p,lambda)) thy =
    1.23              let
    1.24                  val (thy',th) = rp' p thy
    1.25              in
    1.26 -                P.INST_TYPE lambda th thy'
    1.27 +                ProofKernel.INST_TYPE lambda th thy'
    1.28              end
    1.29            | rp (PSubst(prfs,ctxt,prf)) thy =
    1.30              let
    1.31 @@ -34,52 +32,52 @@
    1.32                                             end) prfs (thy,[])
    1.33                  val (thy'',th) = rp' prf thy'
    1.34              in
    1.35 -                P.SUBST ths ctxt th thy''
    1.36 +                ProofKernel.SUBST ths ctxt th thy''
    1.37              end
    1.38            | rp (PAbs(prf,v)) thy =
    1.39              let
    1.40                  val (thy',th) = rp' prf thy
    1.41              in
    1.42 -                P.ABS v th thy'
    1.43 +                ProofKernel.ABS v th thy'
    1.44              end
    1.45            | rp (PDisch(prf,tm)) thy =
    1.46              let
    1.47                  val (thy',th) = rp' prf thy
    1.48              in
    1.49 -                P.DISCH tm th thy'
    1.50 +                ProofKernel.DISCH tm th thy'
    1.51              end
    1.52            | rp (PMp(prf1,prf2)) thy =
    1.53              let
    1.54                  val (thy1,th1) = rp' prf1 thy
    1.55                  val (thy2,th2) = rp' prf2 thy1
    1.56              in
    1.57 -                P.MP th1 th2 thy2
    1.58 +                ProofKernel.MP th1 th2 thy2
    1.59              end
    1.60 -          | rp (PHyp tm) thy = P.ASSUME tm thy
    1.61 +          | rp (PHyp tm) thy = ProofKernel.ASSUME tm thy
    1.62            | rp (PDef(seg,name,rhs)) thy =
    1.63 -            (case P.get_def seg name rhs thy of
    1.64 +            (case ProofKernel.get_def seg name rhs thy of
    1.65                   (thy',SOME res) => (thy',res)
    1.66                 | (thy',NONE) => 
    1.67                   if seg = thyname
    1.68 -                 then P.new_definition seg name rhs thy'
    1.69 +                 then ProofKernel.new_definition seg name rhs thy'
    1.70                   else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname))
    1.71 -          | rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
    1.72 +          | rp (POracle(tg,asl,c)) thy = (*ProofKernel.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
    1.73            | rp (PSpec(prf,tm)) thy =
    1.74              let
    1.75                  val (thy',th) = rp' prf thy
    1.76              in
    1.77 -                P.SPEC tm th thy'
    1.78 +                ProofKernel.SPEC tm th thy'
    1.79              end
    1.80            | rp (PInst(prf,theta)) thy =
    1.81              let
    1.82                  val (thy',th) = rp' prf thy
    1.83              in
    1.84 -                P.INST theta th thy'
    1.85 +                ProofKernel.INST theta th thy'
    1.86              end
    1.87            | rp (PGen(prf,v)) thy =
    1.88              let
    1.89                  val (thy',th) = rp' prf thy
    1.90 -                val p = P.GEN v th thy'
    1.91 +                val p = ProofKernel.GEN v th thy'
    1.92              in
    1.93                  p
    1.94              end
    1.95 @@ -87,91 +85,91 @@
    1.96              let
    1.97                  val (thy',th) = rp' prf thy
    1.98              in
    1.99 -                P.GEN_ABS opt vl th thy'
   1.100 +                ProofKernel.GEN_ABS opt vl th thy'
   1.101              end
   1.102            | rp (PImpAS(prf1,prf2)) thy =
   1.103              let
   1.104                  val (thy1,th1) = rp' prf1 thy
   1.105                  val (thy2,th2) = rp' prf2 thy1
   1.106              in
   1.107 -                P.IMP_ANTISYM th1 th2 thy2
   1.108 +                ProofKernel.IMP_ANTISYM th1 th2 thy2
   1.109              end
   1.110            | rp (PSym prf) thy =
   1.111              let
   1.112                  val (thy1,th) = rp' prf thy
   1.113              in
   1.114 -                P.SYM th thy1
   1.115 +                ProofKernel.SYM th thy1
   1.116              end
   1.117            | rp (PTrans(prf1,prf2)) thy =
   1.118              let
   1.119                  val (thy1,th1) = rp' prf1 thy
   1.120                  val (thy2,th2) = rp' prf2 thy1
   1.121              in
   1.122 -                P.TRANS th1 th2 thy2
   1.123 +                ProofKernel.TRANS th1 th2 thy2
   1.124              end
   1.125            | rp (PComb(prf1,prf2)) thy =
   1.126              let
   1.127                  val (thy1,th1) = rp' prf1 thy
   1.128                  val (thy2,th2) = rp' prf2 thy1
   1.129              in
   1.130 -                P.COMB th1 th2 thy2
   1.131 +                ProofKernel.COMB th1 th2 thy2
   1.132              end
   1.133            | rp (PEqMp(prf1,prf2)) thy =
   1.134              let
   1.135                  val (thy1,th1) = rp' prf1 thy
   1.136                  val (thy2,th2) = rp' prf2 thy1
   1.137              in
   1.138 -                P.EQ_MP th1 th2 thy2
   1.139 +                ProofKernel.EQ_MP th1 th2 thy2
   1.140              end
   1.141            | rp (PEqImp prf) thy =
   1.142              let
   1.143                  val (thy',th) = rp' prf thy
   1.144              in
   1.145 -                P.EQ_IMP_RULE th thy'
   1.146 +                ProofKernel.EQ_IMP_RULE th thy'
   1.147              end
   1.148            | rp (PExists(prf,ex,wit)) thy =
   1.149              let
   1.150                  val (thy',th) = rp' prf thy
   1.151              in
   1.152 -                P.EXISTS ex wit th thy'
   1.153 +                ProofKernel.EXISTS ex wit th thy'
   1.154              end
   1.155            | rp (PChoose(v,prf1,prf2)) thy =
   1.156              let
   1.157                  val (thy1,th1) = rp' prf1 thy
   1.158                  val (thy2,th2) = rp' prf2 thy1
   1.159              in
   1.160 -                P.CHOOSE v th1 th2 thy2
   1.161 +                ProofKernel.CHOOSE v th1 th2 thy2
   1.162              end
   1.163            | rp (PConj(prf1,prf2)) thy =
   1.164              let
   1.165                  val (thy1,th1) = rp' prf1 thy
   1.166                  val (thy2,th2) = rp' prf2 thy1
   1.167              in
   1.168 -                P.CONJ th1 th2 thy2
   1.169 +                ProofKernel.CONJ th1 th2 thy2
   1.170              end
   1.171            | rp (PConjunct1 prf) thy =
   1.172              let
   1.173                  val (thy',th) = rp' prf thy
   1.174              in
   1.175 -                P.CONJUNCT1 th thy'
   1.176 +                ProofKernel.CONJUNCT1 th thy'
   1.177              end
   1.178            | rp (PConjunct2 prf) thy =
   1.179              let
   1.180                  val (thy',th) = rp' prf thy
   1.181              in
   1.182 -                P.CONJUNCT2 th thy'
   1.183 +                ProofKernel.CONJUNCT2 th thy'
   1.184              end
   1.185            | rp (PDisj1(prf,tm)) thy =
   1.186              let
   1.187                  val (thy',th) = rp' prf thy
   1.188              in
   1.189 -                P.DISJ1 th tm thy'
   1.190 +                ProofKernel.DISJ1 th tm thy'
   1.191              end
   1.192            | rp (PDisj2(prf,tm)) thy =
   1.193              let
   1.194                  val (thy',th) = rp' prf thy
   1.195              in
   1.196 -                P.DISJ2 tm th thy'
   1.197 +                ProofKernel.DISJ2 tm th thy'
   1.198              end
   1.199            | rp (PDisjCases(prf,prf1,prf2)) thy =
   1.200              let
   1.201 @@ -179,25 +177,25 @@
   1.202                  val (thy1,th1) = rp' prf1 thy'
   1.203                  val (thy2,th2) = rp' prf2 thy1
   1.204              in
   1.205 -                P.DISJ_CASES th th1 th2 thy2
   1.206 +                ProofKernel.DISJ_CASES th th1 th2 thy2
   1.207              end
   1.208            | rp (PNotI prf) thy =
   1.209              let
   1.210                  val (thy',th) = rp' prf thy
   1.211              in
   1.212 -                P.NOT_INTRO th thy'
   1.213 +                ProofKernel.NOT_INTRO th thy'
   1.214              end
   1.215            | rp (PNotE prf) thy =
   1.216              let
   1.217                  val (thy',th) = rp' prf thy
   1.218              in
   1.219 -                P.NOT_ELIM th thy'
   1.220 +                ProofKernel.NOT_ELIM th thy'
   1.221              end
   1.222            | rp (PContr(prf,tm)) thy =
   1.223              let
   1.224                  val (thy',th) = rp' prf thy
   1.225              in
   1.226 -                P.CCONTR tm th thy'
   1.227 +                ProofKernel.CCONTR tm th thy'
   1.228              end
   1.229            | rp (PTmSpec _) _ = raise ERR "rp" "Shouldn't reach here (PTmSpec)"
   1.230            | rp (PTyDef _) _ = raise ERR "rp" "Shouldn't reach here (PTyDef)"
   1.231 @@ -226,7 +224,7 @@
   1.232                                                | SOME th => (thy,th))
   1.233                                         else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
   1.234                                       | NONE => 
   1.235 -                                       (case P.get_thm thyname' thmname thy of
   1.236 +                                       (case ProofKernel.get_thm thyname' thmname thy of
   1.237                                              (thy',SOME res) => (thy',res)
   1.238                                            | (thy',NONE) => 
   1.239                                              if thyname' = thyname
   1.240 @@ -242,31 +240,31 @@
   1.241                                                          PTmSpec _ => (thy',th)
   1.242                                                        | PTyDef  _ => (thy',th)
   1.243                                                        | PTyIntro _ => (thy',th)
   1.244 -                                                      | _ => P.store_thm thyname' thmname th thy'
   1.245 +                                                      | _ => ProofKernel.store_thm thyname' thmname th thy'
   1.246                                                  end
   1.247                                              else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")))
   1.248                                  | NONE => raise ERR "rp'.PDisk" "Not enough information")
   1.249                    | PAxm(name,c) =>
   1.250 -                    (case P.get_axiom thyname name thy of
   1.251 +                    (case ProofKernel.get_axiom thyname name thy of
   1.252                              (thy',SOME res) => (thy',res)
   1.253 -                          | (thy',NONE) => P.new_axiom name c thy')
   1.254 +                          | (thy',NONE) => ProofKernel.new_axiom name c thy')
   1.255                    | PTmSpec(seg,names,prf') =>
   1.256                      let
   1.257                          val (thy',th) = rp' prf' thy
   1.258                      in
   1.259 -                        P.new_specification seg thmname names th thy'
   1.260 +                        ProofKernel.new_specification seg thmname names th thy'
   1.261                      end
   1.262                    | PTyDef(seg,name,prf') =>
   1.263                      let
   1.264                          val (thy',th) = rp' prf' thy
   1.265                      in
   1.266 -                        P.new_type_definition seg thmname name th thy'
   1.267 +                        ProofKernel.new_type_definition seg thmname name th thy'
   1.268                      end
   1.269                    | PTyIntro(seg,name,abs_name,rep_name,P,t,prf') =>
   1.270                      let
   1.271                          val (thy',th) = rp' prf' thy
   1.272                      in
   1.273 -                        P.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
   1.274 +                        ProofKernel.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
   1.275                      end
   1.276                    | _ => rp pc thy
   1.277              end
   1.278 @@ -282,7 +280,7 @@
   1.279  fun setup_int_thms thyname thy =
   1.280      let
   1.281          val fname =
   1.282 -            case P.get_proof_dir thyname thy of
   1.283 +            case ProofKernel.get_proof_dir thyname thy of
   1.284                  SOME p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
   1.285                | NONE => error "Cannot find proof files"
   1.286          val is = TextIO.openIn fname
   1.287 @@ -291,7 +289,7 @@
   1.288                  fun get_facts facts =
   1.289                      case TextIO.inputLine is of
   1.290                          NONE => (case facts of
   1.291 -                                   i::facts => (the (Int.fromString i),map P.protect_factname (rev facts))
   1.292 +                                   i::facts => (the (Int.fromString i),map ProofKernel.protect_factname (rev facts))
   1.293                                   | _ => raise ERR "replay_thm" "Bad facts.lst file")
   1.294                        | SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
   1.295              in
   1.296 @@ -349,9 +347,9 @@
   1.297            | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
   1.298              add_hol4_type_mapping thyname tycname true fulltyname thy
   1.299            | delta (Indexed_theorem (i, th)) thy = 
   1.300 -            (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)                   
   1.301 -          | delta (Protect_varname (s,t)) thy = (P.replay_protect_varname s t; thy)
   1.302 -          | delta (Dump s) thy = P.replay_add_dump s thy
   1.303 +            (Array.update (int_thms,i-1,SOME (ProofKernel.to_hol_thm (th_of thy th))); thy)                   
   1.304 +          | delta (Protect_varname (s,t)) thy = (ProofKernel.replay_protect_varname s t; thy)
   1.305 +          | delta (Dump s) thy = ProofKernel.replay_add_dump s thy
   1.306      in
   1.307          rps
   1.308      end
     2.1 --- a/src/HOL/Tools/TFL/dcterm.ML	Wed Dec 15 15:01:34 2010 +0100
     2.2 +++ b/src/HOL/Tools/TFL/dcterm.ML	Wed Dec 15 15:11:56 2010 +0100
     2.3 @@ -49,9 +49,7 @@
     2.4  structure Dcterm: DCTERM =
     2.5  struct
     2.6  
     2.7 -structure U = Utils;
     2.8 -
     2.9 -fun ERR func mesg = U.ERR {module = "Dcterm", func = func, mesg = mesg};
    2.10 +fun ERR func mesg = Utils.ERR {module = "Dcterm", func = func, mesg = mesg};
    2.11  
    2.12  
    2.13  fun dest_comb t = Thm.dest_comb t
    2.14 @@ -110,19 +108,19 @@
    2.15  fun dest_monop expected tm =
    2.16   let
    2.17     fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected);
    2.18 -   val (c, N) = dest_comb tm handle U.ERR _ => err ();
    2.19 -   val name = #Name (dest_const c handle U.ERR _ => err ());
    2.20 +   val (c, N) = dest_comb tm handle Utils.ERR _ => err ();
    2.21 +   val name = #Name (dest_const c handle Utils.ERR _ => err ());
    2.22   in if name = expected then N else err () end;
    2.23  
    2.24  fun dest_binop expected tm =
    2.25   let
    2.26     fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected);
    2.27 -   val (M, N) = dest_comb tm handle U.ERR _ => err ()
    2.28 - in (dest_monop expected M, N) handle U.ERR _ => err () end;
    2.29 +   val (M, N) = dest_comb tm handle Utils.ERR _ => err ()
    2.30 + in (dest_monop expected M, N) handle Utils.ERR _ => err () end;
    2.31  
    2.32  fun dest_binder expected tm =
    2.33    dest_abs NONE (dest_monop expected tm)
    2.34 -  handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
    2.35 +  handle Utils.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
    2.36  
    2.37  
    2.38  val dest_neg    = dest_monop @{const_name Not}
    2.39 @@ -151,7 +149,7 @@
    2.40  (*---------------------------------------------------------------------------
    2.41   * Iterated creation.
    2.42   *---------------------------------------------------------------------------*)
    2.43 -val list_mk_disj = U.end_itlist (fn d1 => fn tm => mk_disj (d1, tm));
    2.44 +val list_mk_disj = Utils.end_itlist (fn d1 => fn tm => mk_disj (d1, tm));
    2.45  
    2.46  (*---------------------------------------------------------------------------
    2.47   * Iterated destruction. (To the "right" in a term.)
    2.48 @@ -160,7 +158,7 @@
    2.49    let fun dest (p as (ctm,accum)) =
    2.50          let val (M,N) = break ctm
    2.51          in dest (N, M::accum)
    2.52 -        end handle U.ERR _ => p
    2.53 +        end handle Utils.ERR _ => p
    2.54    in dest (tm,[])
    2.55    end;
    2.56  
    2.57 @@ -190,7 +188,7 @@
    2.58    handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
    2.59      | TERM (msg, _) => raise ERR "mk_prop" msg;
    2.60  
    2.61 -fun drop_prop ctm = dest_monop @{const_name Trueprop} ctm handle U.ERR _ => ctm;
    2.62 +fun drop_prop ctm = dest_monop @{const_name Trueprop} ctm handle Utils.ERR _ => ctm;
    2.63  
    2.64  
    2.65  end;
     3.1 --- a/src/HOL/Tools/TFL/post.ML	Wed Dec 15 15:01:34 2010 +0100
     3.2 +++ b/src/HOL/Tools/TFL/post.ML	Wed Dec 15 15:11:56 2010 +0100
     3.3 @@ -18,8 +18,6 @@
     3.4  structure Tfl: TFL =
     3.5  struct
     3.6  
     3.7 -structure S = USyntax
     3.8 -
     3.9  (* misc *)
    3.10  
    3.11  (*---------------------------------------------------------------------------
    3.12 @@ -53,16 +51,14 @@
    3.13   * processing from the definition stage.
    3.14   *---------------------------------------------------------------------------*)
    3.15  local
    3.16 -structure R = Rules
    3.17 -structure U = Utils
    3.18  
    3.19  (* The rest of these local definitions are for the tricky nested case *)
    3.20 -val solved = not o can S.dest_eq o #2 o S.strip_forall o concl
    3.21 +val solved = not o can USyntax.dest_eq o #2 o USyntax.strip_forall o concl
    3.22  
    3.23  fun id_thm th =
    3.24 -   let val {lhs,rhs} = S.dest_eq (#2 (S.strip_forall (#2 (R.dest_thm th))));
    3.25 +   let val {lhs,rhs} = USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (Rules.dest_thm th))));
    3.26     in lhs aconv rhs end
    3.27 -   handle U.ERR _ => false;
    3.28 +   handle Utils.ERR _ => false;
    3.29     
    3.30  val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
    3.31  fun mk_meta_eq r = case concl_of r of
    3.32 @@ -76,16 +72,16 @@
    3.33  fun join_assums th =
    3.34    let val thy = Thm.theory_of_thm th
    3.35        val tych = cterm_of thy
    3.36 -      val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
    3.37 -      val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
    3.38 -      val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
    3.39 +      val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
    3.40 +      val cntxtl = (#1 o USyntax.strip_imp) lhs  (* cntxtl should = cntxtr *)
    3.41 +      val cntxtr = (#1 o USyntax.strip_imp) rhs  (* but union is solider *)
    3.42        val cntxt = union (op aconv) cntxtl cntxtr
    3.43    in
    3.44 -    R.GEN_ALL
    3.45 -      (R.DISCH_ALL
    3.46 -         (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
    3.47 +    Rules.GEN_ALL
    3.48 +      (Rules.DISCH_ALL
    3.49 +         (rewrite (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
    3.50    end
    3.51 -  val gen_all = S.gen_all
    3.52 +  val gen_all = USyntax.gen_all
    3.53  in
    3.54  fun proof_stage strict cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} =
    3.55    let
    3.56 @@ -117,7 +113,7 @@
    3.57            in
    3.58            {induction = induction',
    3.59                 rules = rules',
    3.60 -                 tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
    3.61 +                 tcs = map (gen_all o USyntax.rhs o #2 o USyntax.strip_forall o concl)
    3.62                             (simplified@stubborn)}
    3.63            end
    3.64    end;
    3.65 @@ -144,8 +140,8 @@
    3.66         val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
    3.67         val {rules,rows,TCs,full_pats_TCs} =
    3.68             Prim.post_definition congs (thy, (def,pats))
    3.69 -       val {lhs=f,rhs} = S.dest_eq (concl def)
    3.70 -       val (_,[R,_]) = S.strip_comb rhs
    3.71 +       val {lhs=f,rhs} = USyntax.dest_eq (concl def)
    3.72 +       val (_,[R,_]) = USyntax.strip_comb rhs
    3.73         val dummy = Prim.trace_thms "congs =" congs
    3.74         (*the next step has caused simplifier looping in some cases*)
    3.75         val {induction, rules, tcs} =
    3.76 @@ -154,12 +150,12 @@
    3.77                  full_pats_TCs = full_pats_TCs,
    3.78                  TCs = TCs}
    3.79         val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
    3.80 -                        (R.CONJUNCTS rules)
    3.81 +                        (Rules.CONJUNCTS rules)
    3.82           in  {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')),
    3.83          rules = ListPair.zip(rules', rows),
    3.84          tcs = (termination_goals rules') @ tcs}
    3.85     end
    3.86 -  handle U.ERR {mesg,func,module} =>
    3.87 +  handle Utils.ERR {mesg,func,module} =>
    3.88                 error (mesg ^
    3.89                        "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
    3.90  
    3.91 @@ -217,7 +213,7 @@
    3.92  fun define strict thy cs ss congs wfs fid R seqs =
    3.93    define_i strict thy cs ss congs wfs fid
    3.94        (Syntax.read_term_global thy R) (map (Syntax.read_term_global thy) seqs)
    3.95 -    handle U.ERR {mesg,...} => error mesg;
    3.96 +    handle Utils.ERR {mesg,...} => error mesg;
    3.97  
    3.98  
    3.99  (*---------------------------------------------------------------------------
   3.100 @@ -227,11 +223,11 @@
   3.101   *---------------------------------------------------------------------------*)
   3.102  
   3.103  fun func_of_cond_eqn tm =
   3.104 -  #1 (S.strip_comb (#lhs (S.dest_eq (#2 (S.strip_forall (#2 (S.strip_imp tm)))))));
   3.105 +  #1 (USyntax.strip_comb (#lhs (USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (USyntax.strip_imp tm)))))));
   3.106  
   3.107  fun defer_i thy congs fid eqs =
   3.108   let val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs
   3.109 -     val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));
   3.110 +     val f = func_of_cond_eqn (concl (Rules.CONJUNCT1 rules handle Utils.ERR _ => rules));
   3.111       val dummy = writeln "Proving induction theorem ...";
   3.112       val induction = Prim.mk_induction theory
   3.113                          {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
   3.114 @@ -243,7 +239,7 @@
   3.115  
   3.116  fun defer thy congs fid seqs =
   3.117    defer_i thy congs fid (map (Syntax.read_term_global thy) seqs)
   3.118 -    handle U.ERR {mesg,...} => error mesg;
   3.119 +    handle Utils.ERR {mesg,...} => error mesg;
   3.120  end;
   3.121  
   3.122  end;
     4.1 --- a/src/HOL/Tools/TFL/rules.ML	Wed Dec 15 15:01:34 2010 +0100
     4.2 +++ b/src/HOL/Tools/TFL/rules.ML	Wed Dec 15 15:11:56 2010 +0100
     4.3 @@ -57,16 +57,11 @@
     4.4  structure Rules: RULES =
     4.5  struct
     4.6  
     4.7 -structure S = USyntax;
     4.8 -structure U = Utils;
     4.9 -structure D = Dcterm;
    4.10 +fun RULES_ERR func mesg = Utils.ERR {module = "Rules", func = func, mesg = mesg};
    4.11  
    4.12  
    4.13 -fun RULES_ERR func mesg = U.ERR {module = "Rules", func = func, mesg = mesg};
    4.14 -
    4.15 -
    4.16 -fun cconcl thm = D.drop_prop (#prop (Thm.crep_thm thm));
    4.17 -fun chyps thm = map D.drop_prop (#hyps (Thm.crep_thm thm));
    4.18 +fun cconcl thm = Dcterm.drop_prop (#prop (Thm.crep_thm thm));
    4.19 +fun chyps thm = map Dcterm.drop_prop (#hyps (Thm.crep_thm thm));
    4.20  
    4.21  fun dest_thm thm =
    4.22    let val {prop,hyps,...} = Thm.rep_thm thm
    4.23 @@ -95,7 +90,7 @@
    4.24    handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg;
    4.25  
    4.26  fun rbeta th =
    4.27 -  (case D.strip_comb (cconcl th) of
    4.28 +  (case Dcterm.strip_comb (cconcl th) of
    4.29      (_, [l, r]) => Thm.transitive th (Thm.beta_conversion false r)
    4.30    | _ => raise RULES_ERR "rbeta" "");
    4.31  
    4.32 @@ -108,7 +103,7 @@
    4.33   * "B" results in something that looks like "A --> B".
    4.34   *---------------------------------------------------------------------------*)
    4.35  
    4.36 -fun ASSUME ctm = Thm.assume (D.mk_prop ctm);
    4.37 +fun ASSUME ctm = Thm.assume (Dcterm.mk_prop ctm);
    4.38  
    4.39  
    4.40  (*---------------------------------------------------------------------------
    4.41 @@ -119,7 +114,7 @@
    4.42    handle THM (msg, _, _) => raise RULES_ERR "MP" msg;
    4.43  
    4.44  (*forces the first argument to be a proposition if necessary*)
    4.45 -fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI
    4.46 +fun DISCH tm thm = Thm.implies_intr (Dcterm.mk_prop tm) thm COMP impI
    4.47    handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
    4.48  
    4.49  fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm;
    4.50 @@ -131,9 +126,9 @@
    4.51   end;
    4.52  
    4.53  fun UNDISCH thm =
    4.54 -   let val tm = D.mk_prop (#1 (D.dest_imp (cconcl thm)))
    4.55 +   let val tm = Dcterm.mk_prop (#1 (Dcterm.dest_imp (cconcl thm)))
    4.56     in Thm.implies_elim (thm RS mp) (ASSUME tm) end
    4.57 -   handle U.ERR _ => raise RULES_ERR "UNDISCH" ""
    4.58 +   handle Utils.ERR _ => raise RULES_ERR "UNDISCH" ""
    4.59       | THM _ => raise RULES_ERR "UNDISCH" "";
    4.60  
    4.61  fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;
    4.62 @@ -152,7 +147,7 @@
    4.63  fun CONJUNCT2 thm = thm RS conjunct2
    4.64    handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg;
    4.65  
    4.66 -fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle U.ERR _ => [th];
    4.67 +fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle Utils.ERR _ => [th];
    4.68  
    4.69  fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list"
    4.70    | LIST_CONJ [th] = th
    4.71 @@ -168,7 +163,7 @@
    4.72        val [P,Q] = OldTerm.term_vars prop
    4.73        val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
    4.74  in
    4.75 -fun DISJ1 thm tm = thm RS (Thm.forall_elim (D.drop_prop tm) disj1)
    4.76 +fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1)
    4.77    handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
    4.78  end;
    4.79  
    4.80 @@ -177,7 +172,7 @@
    4.81        val [P,Q] = OldTerm.term_vars prop
    4.82        val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
    4.83  in
    4.84 -fun DISJ2 tm thm = thm RS (Thm.forall_elim (D.drop_prop tm) disj2)
    4.85 +fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
    4.86    handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
    4.87  end;
    4.88  
    4.89 @@ -195,10 +190,10 @@
    4.90    let fun blue ldisjs [] _ = []
    4.91          | blue ldisjs (th::rst) rdisjs =
    4.92              let val tail = tl rdisjs
    4.93 -                val rdisj_tl = D.list_mk_disj tail
    4.94 +                val rdisj_tl = Dcterm.list_mk_disj tail
    4.95              in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl)
    4.96                 :: blue (ldisjs @ [cconcl th]) rst tail
    4.97 -            end handle U.ERR _ => [fold_rev DISJ2 ldisjs th]
    4.98 +            end handle Utils.ERR _ => [fold_rev DISJ2 ldisjs th]
    4.99     in blue [] thms (map cconcl thms) end;
   4.100  
   4.101  
   4.102 @@ -212,8 +207,8 @@
   4.103  
   4.104  fun DISJ_CASES th1 th2 th3 =
   4.105    let
   4.106 -    val c = D.drop_prop (cconcl th1);
   4.107 -    val (disj1, disj2) = D.dest_disj c;
   4.108 +    val c = Dcterm.drop_prop (cconcl th1);
   4.109 +    val (disj1, disj2) = Dcterm.dest_disj c;
   4.110      val th2' = DISCH disj1 th2;
   4.111      val th3' = DISCH disj2 th3;
   4.112    in
   4.113 @@ -253,12 +248,12 @@
   4.114         fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
   4.115                                         aconv term_of atm)
   4.116                                (#hyps(rep_thm th))
   4.117 -       val tml = D.strip_disj c
   4.118 +       val tml = Dcterm.strip_disj c
   4.119         fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"
   4.120           | DL th [th1] = PROVE_HYP th th1
   4.121           | DL th [th1,th2] = DISJ_CASES th th1 th2
   4.122           | DL th (th1::rst) =
   4.123 -            let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
   4.124 +            let val tm = #2 (Dcterm.dest_disj (Dcterm.drop_prop(cconcl th)))
   4.125               in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
   4.126     in DL disjth (organize eq tml thl)
   4.127     end;
   4.128 @@ -279,7 +274,7 @@
   4.129     in thm RS (Thm.forall_elim tm gspec') end
   4.130  end;
   4.131  
   4.132 -fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm;
   4.133 +fun SPEC_ALL thm = fold SPEC (#1 (Dcterm.strip_forall(cconcl thm))) thm;
   4.134  
   4.135  val ISPEC = SPEC
   4.136  val ISPECL = fold ISPEC;
   4.137 @@ -323,7 +318,7 @@
   4.138  
   4.139  
   4.140  fun MATCH_MP th1 th2 =
   4.141 -   if (D.is_forall (D.drop_prop(cconcl th1)))
   4.142 +   if (Dcterm.is_forall (Dcterm.drop_prop(cconcl th1)))
   4.143     then MATCH_MP (th1 RS spec) th2
   4.144     else MP th1 th2;
   4.145  
   4.146 @@ -345,8 +340,8 @@
   4.147  
   4.148  fun CHOOSE (fvar, exth) fact =
   4.149    let
   4.150 -    val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth)))
   4.151 -    val redex = D.capply lam fvar
   4.152 +    val lam = #2 (Dcterm.dest_comb (Dcterm.drop_prop (cconcl exth)))
   4.153 +    val redex = Dcterm.capply lam fvar
   4.154      val thy = Thm.theory_of_cterm redex
   4.155      val t$u = Thm.term_of redex
   4.156      val residue = Thm.cterm_of thy (Term.betapply (t, u))
   4.157 @@ -364,7 +359,7 @@
   4.158         val prop = Thm.prop_of thm
   4.159         val P' = cterm_of thy P
   4.160         val x' = cterm_of thy x
   4.161 -       val abstr = #2 (D.dest_comb template)
   4.162 +       val abstr = #2 (Dcterm.dest_comb template)
   4.163     in
   4.164     thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
   4.165       handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
   4.166 @@ -380,7 +375,7 @@
   4.167   *---------------------------------------------------------------------------*)
   4.168  
   4.169  fun EXISTL vlist th =
   4.170 -  fold_rev (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)
   4.171 +  fold_rev (fn v => fn thm => EXISTS(Dcterm.mk_exists(v,cconcl thm), v) thm)
   4.172             vlist th;
   4.173  
   4.174  
   4.175 @@ -397,7 +392,7 @@
   4.176     let val thy = Thm.theory_of_thm th
   4.177         val tych = cterm_of thy
   4.178         val blist' = map (pairself Thm.term_of) blist
   4.179 -       fun ex v M  = cterm_of thy (S.mk_exists{Bvar=v,Body = M})
   4.180 +       fun ex v M  = cterm_of thy (USyntax.mk_exists{Bvar=v,Body = M})
   4.181  
   4.182    in
   4.183    fold_rev (fn (b as (r1,r2)) => fn thm =>
   4.184 @@ -443,7 +438,7 @@
   4.185  
   4.186  
   4.187  (* Object language quantifier, i.e., "!" *)
   4.188 -fun Forall v M = S.mk_forall{Bvar=v, Body=M};
   4.189 +fun Forall v M = USyntax.mk_forall{Bvar=v, Body=M};
   4.190  
   4.191  
   4.192  (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
   4.193 @@ -458,11 +453,11 @@
   4.194                 (Const (@{const_name Trueprop},_) $ lhs)
   4.195                 $ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs}
   4.196    | dest_equal(Const ("==",_) $ lhs $ rhs)  = {lhs=lhs, rhs=rhs}
   4.197 -  | dest_equal tm = S.dest_eq tm;
   4.198 +  | dest_equal tm = USyntax.dest_eq tm;
   4.199  
   4.200  fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
   4.201  
   4.202 -fun dest_all used (Const("all",_) $ (a as Abs _)) = S.dest_abs used a
   4.203 +fun dest_all used (Const("all",_) $ (a as Abs _)) = USyntax.dest_abs used a
   4.204    | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";
   4.205  
   4.206  val is_all = can (dest_all []);
   4.207 @@ -505,13 +500,13 @@
   4.208          of ([],_) => get (rst, n+1,L)
   4.209           | (vlist,body) =>
   4.210              let val eq = Logic.strip_imp_concl body
   4.211 -                val (f,args) = S.strip_comb (get_lhs eq)
   4.212 -                val (vstrl,_) = S.strip_abs f
   4.213 +                val (f,args) = USyntax.strip_comb (get_lhs eq)
   4.214 +                val (vstrl,_) = USyntax.strip_abs f
   4.215                  val names  =
   4.216                    Name.variant_list (OldTerm.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
   4.217              in get (rst, n+1, (names,n)::L) end
   4.218              handle TERM _ => get (rst, n+1, L)
   4.219 -              | U.ERR _ => get (rst, n+1, L);
   4.220 +              | Utils.ERR _ => get (rst, n+1, L);
   4.221  
   4.222  (* Note: Thm.rename_params_rule counts from 1, not 0 *)
   4.223  fun rename thm =
   4.224 @@ -529,7 +524,7 @@
   4.225   *---------------------------------------------------------------------------*)
   4.226  
   4.227  fun list_beta_conv tm =
   4.228 -  let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(D.dest_eq(cconcl th))))
   4.229 +  let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(Dcterm.dest_eq(cconcl th))))
   4.230        fun iter [] = Thm.reflexive tm
   4.231          | iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v))
   4.232    in iter  end;
   4.233 @@ -553,28 +548,28 @@
   4.234   * General abstraction handlers, should probably go in USyntax.
   4.235   *---------------------------------------------------------------------------*)
   4.236  fun mk_aabs (vstr, body) =
   4.237 -  S.mk_abs {Bvar = vstr, Body = body}
   4.238 -  handle U.ERR _ => S.mk_pabs {varstruct = vstr, body = body};
   4.239 +  USyntax.mk_abs {Bvar = vstr, Body = body}
   4.240 +  handle Utils.ERR _ => USyntax.mk_pabs {varstruct = vstr, body = body};
   4.241  
   4.242  fun list_mk_aabs (vstrl,tm) =
   4.243      fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
   4.244  
   4.245  fun dest_aabs used tm =
   4.246 -   let val ({Bvar,Body}, used') = S.dest_abs used tm
   4.247 +   let val ({Bvar,Body}, used') = USyntax.dest_abs used tm
   4.248     in (Bvar, Body, used') end
   4.249 -   handle U.ERR _ =>
   4.250 -     let val {varstruct, body, used} = S.dest_pabs used tm
   4.251 +   handle Utils.ERR _ =>
   4.252 +     let val {varstruct, body, used} = USyntax.dest_pabs used tm
   4.253       in (varstruct, body, used) end;
   4.254  
   4.255  fun strip_aabs used tm =
   4.256     let val (vstr, body, used') = dest_aabs used tm
   4.257         val (bvs, core, used'') = strip_aabs used' body
   4.258     in (vstr::bvs, core, used'') end
   4.259 -   handle U.ERR _ => ([], tm, used);
   4.260 +   handle Utils.ERR _ => ([], tm, used);
   4.261  
   4.262  fun dest_combn tm 0 = (tm,[])
   4.263    | dest_combn tm n =
   4.264 -     let val {Rator,Rand} = S.dest_comb tm
   4.265 +     let val {Rator,Rand} = USyntax.dest_comb tm
   4.266           val (f,rands) = dest_combn Rator (n-1)
   4.267       in (f,Rand::rands)
   4.268       end;
   4.269 @@ -582,7 +577,7 @@
   4.270  
   4.271  
   4.272  
   4.273 -local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
   4.274 +local fun dest_pair M = let val {fst,snd} = USyntax.dest_pair M in (fst,snd) end
   4.275        fun mk_fst tm =
   4.276            let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
   4.277            in  Const ("Product_Type.fst", ty --> fty) $ tm  end
   4.278 @@ -610,7 +605,7 @@
   4.279   *---------------------------------------------------------------------------*)
   4.280  
   4.281  fun VSTRUCT_ELIM tych a vstr th =
   4.282 -  let val L = S.free_vars_lr vstr
   4.283 +  let val L = USyntax.free_vars_lr vstr
   4.284        val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
   4.285        val thm1 = Thm.implies_intr bind1 (SUBS [SYM(Thm.assume bind1)] th)
   4.286        val thm2 = forall_intr_list (map tych L) thm1
   4.287 @@ -641,7 +636,7 @@
   4.288    in (strip_aabs used f,args)
   4.289    end;
   4.290  
   4.291 -fun pbeta_redex M n = can (U.C (dest_pbeta_redex []) n) M;
   4.292 +fun pbeta_redex M n = can (Utils.C (dest_pbeta_redex []) n) M;
   4.293  
   4.294  fun dest_impl tm =
   4.295    let val ants = Logic.strip_imp_prems tm
   4.296 @@ -649,7 +644,7 @@
   4.297    in (ants,get_lhs eq)
   4.298    end;
   4.299  
   4.300 -fun restricted t = is_some (S.find_term
   4.301 +fun restricted t = is_some (USyntax.find_term
   4.302                              (fn (Const(@{const_name Recdef.cut},_)) =>true | _ => false)
   4.303                              t)
   4.304  
   4.305 @@ -675,7 +670,7 @@
   4.306                       val lhs = tych(get_lhs eq)
   4.307                       val ss' = Simplifier.add_prems (map ASSUME ants) ss
   4.308                       val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs
   4.309 -                       handle U.ERR _ => Thm.reflexive lhs
   4.310 +                       handle Utils.ERR _ => Thm.reflexive lhs
   4.311                       val dummy = print_thms "proven:" [lhs_eq_lhs1]
   4.312                       val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
   4.313                       val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
   4.314 @@ -693,10 +688,10 @@
   4.315                    val eq1 = Logic.strip_imp_concl imp_body1
   4.316                    val Q = get_lhs eq1
   4.317                    val QeqQ1 = pbeta_reduce (tych Q)
   4.318 -                  val Q1 = #2(D.dest_eq(cconcl QeqQ1))
   4.319 +                  val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1))
   4.320                    val ss' = Simplifier.add_prems (map ASSUME ants1) ss
   4.321                    val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1
   4.322 -                                handle U.ERR _ => Thm.reflexive Q1
   4.323 +                                handle Utils.ERR _ => Thm.reflexive Q1
   4.324                    val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
   4.325                    val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
   4.326                    val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
   4.327 @@ -708,7 +703,7 @@
   4.328                    val impth = implies_intr_list ants1 QeeqQ3
   4.329                    val impth1 = impth RS meta_eq_to_obj_eq
   4.330                    (* Need to abstract *)
   4.331 -                  val ant_th = U.itlist2 (PGEN tych) args vstrl impth1
   4.332 +                  val ant_th = Utils.itlist2 (PGEN tych) args vstrl impth1
   4.333                in ant_th COMP thm
   4.334                end
   4.335               fun q_eliminate (thm,imp,thy) =
   4.336 @@ -722,7 +717,7 @@
   4.337                       val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
   4.338                       val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
   4.339                          (false,true,false) (prover used') ss' (tych Q)
   4.340 -                      handle U.ERR _ => Thm.reflexive (tych Q)
   4.341 +                      handle Utils.ERR _ => Thm.reflexive (tych Q)
   4.342                       val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
   4.343                       val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
   4.344                       val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
   4.345 @@ -740,7 +735,7 @@
   4.346                              (* Assume that the leading constant is ==,   *)
   4.347                  | _ => thm  (* if it is not a ==>                        *)
   4.348           in SOME(eliminate (rename thm)) end
   4.349 -         handle U.ERR _ => NONE    (* FIXME handle THM as well?? *)
   4.350 +         handle Utils.ERR _ => NONE    (* FIXME handle THM as well?? *)
   4.351  
   4.352          fun restrict_prover ss thm =
   4.353            let val dummy = say "restrict_prover:"
   4.354 @@ -765,12 +760,12 @@
   4.355                val rcontext = rev cntxt
   4.356                val cncl = HOLogic.dest_Trueprop o Thm.prop_of
   4.357                val antl = case rcontext of [] => []
   4.358 -                         | _   => [S.list_mk_conj(map cncl rcontext)]
   4.359 -              val TC = genl(S.list_mk_imp(antl, A))
   4.360 +                         | _   => [USyntax.list_mk_conj(map cncl rcontext)]
   4.361 +              val TC = genl(USyntax.list_mk_imp(antl, A))
   4.362                val dummy = print_cterm "func:" (cterm_of thy func)
   4.363                val dummy = print_cterm "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC))
   4.364                val dummy = tc_list := (TC :: !tc_list)
   4.365 -              val nestedp = is_some (S.find_term is_func TC)
   4.366 +              val nestedp = is_some (USyntax.find_term is_func TC)
   4.367                val dummy = if nestedp then say "nested" else say "not_nested"
   4.368                val th' = if nestedp then raise RULES_ERR "solver" "nested function"
   4.369                          else let val cTC = cterm_of thy
   4.370 @@ -782,7 +777,7 @@
   4.371                               end
   4.372                val th'' = th' RS thm
   4.373            in SOME (th'')
   4.374 -          end handle U.ERR _ => NONE    (* FIXME handle THM as well?? *)
   4.375 +          end handle Utils.ERR _ => NONE    (* FIXME handle THM as well?? *)
   4.376      in
   4.377      (if (is_cong thm) then cong_prover else restrict_prover) ss thm
   4.378      end
     5.1 --- a/src/HOL/Tools/TFL/tfl.ML	Wed Dec 15 15:01:34 2010 +0100
     5.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Dec 15 15:11:56 2010 +0100
     5.3 @@ -42,17 +42,13 @@
     5.4  
     5.5  val trace = Unsynchronized.ref false;
     5.6  
     5.7 -structure R = Rules;
     5.8 -structure S = USyntax;
     5.9 -structure U = Utils;
    5.10  
    5.11 +fun TFL_ERR func mesg = Utils.ERR {module = "Tfl", func = func, mesg = mesg};
    5.12  
    5.13 -fun TFL_ERR func mesg = U.ERR {module = "Tfl", func = func, mesg = mesg};
    5.14 +val concl = #2 o Rules.dest_thm;
    5.15 +val hyp = #1 o Rules.dest_thm;
    5.16  
    5.17 -val concl = #2 o R.dest_thm;
    5.18 -val hyp = #1 o R.dest_thm;
    5.19 -
    5.20 -val list_mk_type = U.end_itlist (curry (op -->));
    5.21 +val list_mk_type = Utils.end_itlist (curry (op -->));
    5.22  
    5.23  fun front_last [] = raise TFL_ERR "front_last" "empty list"
    5.24    | front_last [x] = ([],x)
    5.25 @@ -99,12 +95,12 @@
    5.26                val (in_group, not_in_group) =
    5.27                 fold_rev (fn (row as (p::rst, rhs)) =>
    5.28                           fn (in_group,not_in_group) =>
    5.29 -                  let val (pc,args) = S.strip_comb p
    5.30 +                  let val (pc,args) = USyntax.strip_comb p
    5.31                    in if (#1(dest_Const pc) = c)
    5.32                       then ((args@rst, rhs)::in_group, not_in_group)
    5.33                       else (in_group, row::not_in_group)
    5.34                    end)      rows ([],[])
    5.35 -              val col_types = U.take type_of (length L, #1(hd in_group))
    5.36 +              val col_types = Utils.take type_of (length L, #1(hd in_group))
    5.37            in
    5.38            part{constrs = crst, rows = not_in_group,
    5.39                 A = {constructor = c,
    5.40 @@ -142,8 +138,8 @@
    5.41        val L = binder_types Ty
    5.42        and ty = body_type Ty
    5.43        val ty_theta = ty_match ty colty
    5.44 -      val c' = S.inst ty_theta c
    5.45 -      val gvars = map (S.inst ty_theta o gv) L
    5.46 +      val c' = USyntax.inst ty_theta c
    5.47 +      val gvars = map (USyntax.inst ty_theta o gv) L
    5.48    in (c', gvars)
    5.49    end;
    5.50  
    5.51 @@ -155,7 +151,7 @@
    5.52  fun mk_group name rows =
    5.53    fold_rev (fn (row as ((prfx, p::rst), rhs)) =>
    5.54              fn (in_group,not_in_group) =>
    5.55 -               let val (pc,args) = S.strip_comb p
    5.56 +               let val (pc,args) = USyntax.strip_comb p
    5.57                 in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false)
    5.58                    then (((prfx,args@rst), rhs)::in_group, not_in_group)
    5.59                    else (in_group, row::not_in_group) end)
    5.60 @@ -174,7 +170,7 @@
    5.61               val (in_group, not_in_group) = mk_group (#1 (dest_Const c')) rows
    5.62               val in_group' =
    5.63                   if (null in_group)  (* Constructor not given *)
    5.64 -                 then [((prfx, #2(fresh c)), (S.ARB res_ty, (~1,false)))]
    5.65 +                 then [((prfx, #2(fresh c)), (USyntax.ARB res_ty, (~1,false)))]
    5.66                   else in_group
    5.67           in
    5.68           part{constrs = crst,
    5.69 @@ -264,7 +260,7 @@
    5.70                             (ListPair.zip (new_formals, groups))
    5.71              val rec_calls = map mk news
    5.72              val (pat_rect,dtrees) = ListPair.unzip rec_calls
    5.73 -            val case_functions = map S.list_mk_abs
    5.74 +            val case_functions = map USyntax.list_mk_abs
    5.75                                    (ListPair.zip (new_formals, dtrees))
    5.76              val types = map type_of (case_functions@[u]) @ [range_ty]
    5.77              val case_const' = Const(case_const_name, list_mk_type types)
    5.78 @@ -279,11 +275,11 @@
    5.79  
    5.80  (* Repeated variable occurrences in a pattern are not allowed. *)
    5.81  fun FV_multiset tm =
    5.82 -   case (S.dest_term tm)
    5.83 -     of S.VAR{Name = c, Ty = T} => [Free(c, T)]
    5.84 -      | S.CONST _ => []
    5.85 -      | S.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
    5.86 -      | S.LAMB _ => raise TFL_ERR "FV_multiset" "lambda";
    5.87 +   case (USyntax.dest_term tm)
    5.88 +     of USyntax.VAR{Name = c, Ty = T} => [Free(c, T)]
    5.89 +      | USyntax.CONST _ => []
    5.90 +      | USyntax.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
    5.91 +      | USyntax.LAMB _ => raise TFL_ERR "FV_multiset" "lambda";
    5.92  
    5.93  fun no_repeat_vars thy pat =
    5.94   let fun check [] = true
    5.95 @@ -370,10 +366,10 @@
    5.96    | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
    5.97  
    5.98  local val f_eq_wfrec_R_M =
    5.99 -           #ant(S.dest_imp(#2(S.strip_forall (concl Thms.WFREC_COROLLARY))))
   5.100 -      val {lhs=f, rhs} = S.dest_eq f_eq_wfrec_R_M
   5.101 +           #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl Thms.WFREC_COROLLARY))))
   5.102 +      val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M
   5.103        val (fname,_) = dest_Free f
   5.104 -      val (wfrec,_) = S.strip_comb rhs
   5.105 +      val (wfrec,_) = USyntax.strip_comb rhs
   5.106  in
   5.107  fun wfrec_definition0 thy fid R (functional as Abs(x, Ty, _)) =
   5.108   let val def_name = Long_Name.base_name fid ^ "_def"
   5.109 @@ -422,15 +418,15 @@
   5.110  
   5.111  fun post_definition meta_tflCongs (theory, (def, pats)) =
   5.112   let val tych = Thry.typecheck theory
   5.113 -     val f = #lhs(S.dest_eq(concl def))
   5.114 -     val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
   5.115 +     val f = #lhs(USyntax.dest_eq(concl def))
   5.116 +     val corollary = Rules.MATCH_MP Thms.WFREC_COROLLARY def
   5.117       val pats' = filter given pats
   5.118       val given_pats = map pat_of pats'
   5.119       val rows = map row_of_pat pats'
   5.120 -     val WFR = #ant(S.dest_imp(concl corollary))
   5.121 -     val R = #Rand(S.dest_comb WFR)
   5.122 -     val corollary' = R.UNDISCH corollary  (* put WF R on assums *)
   5.123 -     val corollaries = map (fn pat => R.SPEC (tych pat) corollary')
   5.124 +     val WFR = #ant(USyntax.dest_imp(concl corollary))
   5.125 +     val R = #Rand(USyntax.dest_comb WFR)
   5.126 +     val corollary' = Rules.UNDISCH corollary  (* put WF R on assums *)
   5.127 +     val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary')
   5.128                             given_pats
   5.129       val (case_rewrites,context_congs) = extraction_thms theory
   5.130       (*case_ss causes minimal simplification: bodies of case expressions are
   5.131 @@ -440,12 +436,12 @@
   5.132         (HOL_basic_ss addcongs
   5.133           (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) theory addsimps case_rewrites)
   5.134       val corollaries' = map (Simplifier.simplify case_ss) corollaries
   5.135 -     val extract = R.CONTEXT_REWRITE_RULE
   5.136 +     val extract = Rules.CONTEXT_REWRITE_RULE
   5.137                       (f, [R], @{thm cut_apply}, meta_tflCongs@context_congs)
   5.138       val (rules, TCs) = ListPair.unzip (map extract corollaries')
   5.139       val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
   5.140 -     val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
   5.141 -     val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
   5.142 +     val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
   5.143 +     val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0)
   5.144   in
   5.145   {rules = rules1,
   5.146    rows = rows,
   5.147 @@ -463,8 +459,8 @@
   5.148   *---------------------------------------------------------------------------*)
   5.149  
   5.150  fun wfrec_eqns thy fid tflCongs eqns =
   5.151 - let val {lhs,rhs} = S.dest_eq (hd eqns)
   5.152 -     val (f,args) = S.strip_comb lhs
   5.153 + let val {lhs,rhs} = USyntax.dest_eq (hd eqns)
   5.154 +     val (f,args) = USyntax.strip_comb lhs
   5.155       val (fname,fty) = dest_atom f
   5.156       val (SV,a) = front_last args    (* SV = schematic variables *)
   5.157       val g = list_comb(f,SV)
   5.158 @@ -482,22 +478,22 @@
   5.159                   else ()
   5.160       val (case_rewrites,context_congs) = extraction_thms thy
   5.161       val tych = Thry.typecheck thy
   5.162 -     val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
   5.163 +     val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY
   5.164       val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
   5.165       val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
   5.166                     Rtype)
   5.167 -     val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
   5.168 -     val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
   5.169 +     val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0
   5.170 +     val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM)
   5.171       val dummy =
   5.172             if !trace then
   5.173                 writeln ("ORIGINAL PROTO_DEF: " ^
   5.174                            Syntax.string_of_term_global thy proto_def)
   5.175             else ()
   5.176 -     val R1 = S.rand WFR
   5.177 -     val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
   5.178 -     val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats
   5.179 +     val R1 = USyntax.rand WFR
   5.180 +     val corollary' = Rules.UNDISCH (Rules.UNDISCH WFREC_THM)
   5.181 +     val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
   5.182       val corollaries' = map (rewrite_rule case_rewrites) corollaries
   5.183 -     fun extract X = R.CONTEXT_REWRITE_RULE
   5.184 +     fun extract X = Rules.CONTEXT_REWRITE_RULE
   5.185                         (f, R1::SV, @{thm cut_apply}, tflCongs@context_congs) X
   5.186   in {proto_def = proto_def,
   5.187       SV=SV,
   5.188 @@ -517,8 +513,8 @@
   5.189  fun lazyR_def thy fid tflCongs eqns =
   5.190   let val {proto_def,WFR,pats,extracta,SV} =
   5.191             wfrec_eqns thy fid tflCongs eqns
   5.192 -     val R1 = S.rand WFR
   5.193 -     val f = #lhs(S.dest_eq proto_def)
   5.194 +     val R1 = USyntax.rand WFR
   5.195 +     val f = #lhs(USyntax.dest_eq proto_def)
   5.196       val (extractants,TCl) = ListPair.unzip extracta
   5.197       val dummy = if !trace
   5.198                   then writeln (cat_lines ("Extractants =" ::
   5.199 @@ -526,17 +522,17 @@
   5.200                   else ()
   5.201       val TCs = fold_rev (union (op aconv)) TCl []
   5.202       val full_rqt = WFR::TCs
   5.203 -     val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
   5.204 -     val R'abs = S.rand R'
   5.205 +     val R' = USyntax.mk_select{Bvar=R1, Body=USyntax.list_mk_conj full_rqt}
   5.206 +     val R'abs = USyntax.rand R'
   5.207       val proto_def' = subst_free[(R1,R')] proto_def
   5.208       val dummy = if !trace then writeln ("proto_def' = " ^
   5.209                                           Syntax.string_of_term_global
   5.210                                           thy proto_def')
   5.211                             else ()
   5.212 -     val {lhs,rhs} = S.dest_eq proto_def'
   5.213 -     val (c,args) = S.strip_comb lhs
   5.214 +     val {lhs,rhs} = USyntax.dest_eq proto_def'
   5.215 +     val (c,args) = USyntax.strip_comb lhs
   5.216       val (name,Ty) = dest_atom c
   5.217 -     val defn = const_def thy (name, Ty, S.list_mk_abs (args,rhs))
   5.218 +     val defn = const_def thy (name, Ty, USyntax.list_mk_abs (args,rhs))
   5.219       val ([def0], theory) =
   5.220         thy
   5.221         |> Global_Theory.add_defs false
   5.222 @@ -545,31 +541,31 @@
   5.223       val dummy =
   5.224         if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
   5.225         else ()
   5.226 -     (* val fconst = #lhs(S.dest_eq(concl def))  *)
   5.227 +     (* val fconst = #lhs(USyntax.dest_eq(concl def))  *)
   5.228       val tych = Thry.typecheck theory
   5.229       val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
   5.230           (*lcp: a lot of object-logic inference to remove*)
   5.231 -     val baz = R.DISCH_ALL
   5.232 -                 (fold_rev R.DISCH full_rqt_prop
   5.233 -                  (R.LIST_CONJ extractants))
   5.234 +     val baz = Rules.DISCH_ALL
   5.235 +                 (fold_rev Rules.DISCH full_rqt_prop
   5.236 +                  (Rules.LIST_CONJ extractants))
   5.237       val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm_global theory baz)
   5.238                             else ()
   5.239       val f_free = Free (fid, fastype_of f)  (*'cos f is a Const*)
   5.240       val SV' = map tych SV;
   5.241       val SVrefls = map Thm.reflexive SV'
   5.242 -     val def0 = (fold (fn x => fn th => R.rbeta(Thm.combination th x))
   5.243 +     val def0 = (fold (fn x => fn th => Rules.rbeta(Thm.combination th x))
   5.244                     SVrefls def)
   5.245                  RS meta_eq_to_obj_eq
   5.246 -     val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0
   5.247 -     val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop)
   5.248 +     val def' = Rules.MP (Rules.SPEC (tych R') (Rules.GEN (tych R1) baz)) def0
   5.249 +     val body_th = Rules.LIST_CONJ (map Rules.ASSUME full_rqt_prop)
   5.250       val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon
   5.251                         theory Hilbert_Choice*)
   5.252           ML_Context.thm "Hilbert_Choice.tfl_some"
   5.253           handle ERROR msg => cat_error msg
   5.254      "defer_recdef requires theory Main or at least Hilbert_Choice as parent"
   5.255 -     val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
   5.256 +     val bar = Rules.MP (Rules.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
   5.257   in {theory = theory, R=R1, SV=SV,
   5.258 -     rules = fold (U.C R.MP) (R.CONJUNCTS bar) def',
   5.259 +     rules = fold (Utils.C Rules.MP) (Rules.CONJUNCTS bar) def',
   5.260       full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
   5.261       patterns = pats}
   5.262   end;
   5.263 @@ -603,8 +599,8 @@
   5.264   *---------------------------------------------------------------------------*)
   5.265  
   5.266  fun alpha_ex_unroll (xlist, tm) =
   5.267 -  let val (qvars,body) = S.strip_exists tm
   5.268 -      val vlist = #2(S.strip_comb (S.rhs body))
   5.269 +  let val (qvars,body) = USyntax.strip_exists tm
   5.270 +      val vlist = #2 (USyntax.strip_comb (USyntax.rhs body))
   5.271        val plist = ListPair.zip (vlist, xlist)
   5.272        val args = map (the o AList.lookup (op aconv) plist) qvars
   5.273                     handle Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
   5.274 @@ -634,7 +630,7 @@
   5.275   fun fail s = raise TFL_ERR "mk_case" s
   5.276   fun mk{rows=[],...} = fail"no rows"
   5.277     | mk{path=[], rows = [([], (thm, bindings))]} =
   5.278 -                         R.IT_EXISTS (map tych_binding bindings) thm
   5.279 +                         Rules.IT_EXISTS (map tych_binding bindings) thm
   5.280     | mk{path = u::rstp, rows as (p::_, _)::_} =
   5.281       let val (pat_rectangle,rights) = ListPair.unzip rows
   5.282           val col0 = map hd pat_rectangle
   5.283 @@ -651,8 +647,8 @@
   5.284       case (ty_info ty_name)
   5.285       of NONE => fail("Not a known datatype: "^ty_name)
   5.286        | SOME{constructors,nchotomy} =>
   5.287 -        let val thm' = R.ISPEC (tych u) nchotomy
   5.288 -            val disjuncts = S.strip_disj (concl thm')
   5.289 +        let val thm' = Rules.ISPEC (tych u) nchotomy
   5.290 +            val disjuncts = USyntax.strip_disj (concl thm')
   5.291              val subproblems = divide(constructors, rows)
   5.292              val groups      = map #group subproblems
   5.293              and new_formals = map #new_formals subproblems
   5.294 @@ -660,17 +656,17 @@
   5.295                                     (new_formals, disjuncts)
   5.296              val constraints = map #1 existentials
   5.297              val vexl = map #2 existentials
   5.298 -            fun expnd tm (pats,(th,b)) = (pats,(R.SUBS[R.ASSUME(tych tm)]th,b))
   5.299 +            fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS [Rules.ASSUME (tych tm)] th, b))
   5.300              val news = map (fn (nf,rows,c) => {path = nf@rstp,
   5.301                                                 rows = map (expnd c) rows})
   5.302 -                           (U.zip3 new_formals groups constraints)
   5.303 +                           (Utils.zip3 new_formals groups constraints)
   5.304              val recursive_thms = map mk news
   5.305              val build_exists = Library.foldr
   5.306                                  (fn((x,t), th) =>
   5.307 -                                 R.CHOOSE (tych x, R.ASSUME (tych t)) th)
   5.308 +                                 Rules.CHOOSE (tych x, Rules.ASSUME (tych t)) th)
   5.309              val thms' = ListPair.map build_exists (vexl, recursive_thms)
   5.310 -            val same_concls = R.EVEN_ORS thms'
   5.311 -        in R.DISJ_CASESL thm' same_concls
   5.312 +            val same_concls = Rules.EVEN_ORS thms'
   5.313 +        in Rules.DISJ_CASESL thm' same_concls
   5.314          end
   5.315       end end
   5.316   in mk
   5.317 @@ -688,14 +684,14 @@
   5.318       val a = Free (aname, T)
   5.319       val v = Free (vname, T)
   5.320       val a_eq_v = HOLogic.mk_eq(a,v)
   5.321 -     val ex_th0 = R.EXISTS (tych (S.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
   5.322 -                           (R.REFL (tych a))
   5.323 -     val th0 = R.ASSUME (tych a_eq_v)
   5.324 +     val ex_th0 = Rules.EXISTS (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
   5.325 +                           (Rules.REFL (tych a))
   5.326 +     val th0 = Rules.ASSUME (tych a_eq_v)
   5.327       val rows = map (fn x => ([x], (th0,[]))) pats
   5.328   in
   5.329 - R.GEN (tych a)
   5.330 -       (R.RIGHT_ASSOC
   5.331 -          (R.CHOOSE(tych v, ex_th0)
   5.332 + Rules.GEN (tych a)
   5.333 +       (Rules.RIGHT_ASSOC
   5.334 +          (Rules.CHOOSE(tych v, ex_th0)
   5.335                  (mk_case ty_info (vname::aname::names)
   5.336                   thy {path=[v], rows=rows})))
   5.337   end end;
   5.338 @@ -712,57 +708,57 @@
   5.339   *---------------------------------------------------------------------------*)
   5.340  (*
   5.341  local infix 5 ==>
   5.342 -      fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
   5.343 +      fun (tm1 ==> tm2) = USyntax.mk_imp{ant = tm1, conseq = tm2}
   5.344  in
   5.345  fun build_ih f P (pat,TCs) =
   5.346 - let val globals = S.free_vars_lr pat
   5.347 -     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
   5.348 + let val globals = USyntax.free_vars_lr pat
   5.349 +     fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
   5.350       fun dest_TC tm =
   5.351 -         let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
   5.352 -             val (R,y,_) = S.dest_relation R_y_pat
   5.353 +         let val (cntxt,R_y_pat) = USyntax.strip_imp(#2(USyntax.strip_forall tm))
   5.354 +             val (R,y,_) = USyntax.dest_relation R_y_pat
   5.355               val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
   5.356           in case cntxt
   5.357                of [] => (P_y, (tm,[]))
   5.358                 | _  => let
   5.359 -                    val imp = S.list_mk_conj cntxt ==> P_y
   5.360 -                    val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals)
   5.361 -                    val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs
   5.362 -                    in (S.list_mk_forall(locals,imp), (tm,locals)) end
   5.363 +                    val imp = USyntax.list_mk_conj cntxt ==> P_y
   5.364 +                    val lvs = gen_rems (op aconv) (USyntax.free_vars_lr imp, globals)
   5.365 +                    val locals = #2(Utils.pluck (curry (op aconv) P) lvs) handle Utils.ERR _ => lvs
   5.366 +                    in (USyntax.list_mk_forall(locals,imp), (tm,locals)) end
   5.367           end
   5.368   in case TCs
   5.369 -    of [] => (S.list_mk_forall(globals, P$pat), [])
   5.370 +    of [] => (USyntax.list_mk_forall(globals, P$pat), [])
   5.371       |  _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
   5.372 -                 val ind_clause = S.list_mk_conj ihs ==> P$pat
   5.373 -             in (S.list_mk_forall(globals,ind_clause), TCs_locals)
   5.374 +                 val ind_clause = USyntax.list_mk_conj ihs ==> P$pat
   5.375 +             in (USyntax.list_mk_forall(globals,ind_clause), TCs_locals)
   5.376               end
   5.377   end
   5.378  end;
   5.379  *)
   5.380  
   5.381  local infix 5 ==>
   5.382 -      fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
   5.383 +      fun (tm1 ==> tm2) = USyntax.mk_imp{ant = tm1, conseq = tm2}
   5.384  in
   5.385  fun build_ih f (P,SV) (pat,TCs) =
   5.386 - let val pat_vars = S.free_vars_lr pat
   5.387 + let val pat_vars = USyntax.free_vars_lr pat
   5.388       val globals = pat_vars@SV
   5.389 -     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
   5.390 +     fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
   5.391       fun dest_TC tm =
   5.392 -         let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
   5.393 -             val (R,y,_) = S.dest_relation R_y_pat
   5.394 +         let val (cntxt,R_y_pat) = USyntax.strip_imp(#2(USyntax.strip_forall tm))
   5.395 +             val (R,y,_) = USyntax.dest_relation R_y_pat
   5.396               val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
   5.397           in case cntxt
   5.398                of [] => (P_y, (tm,[]))
   5.399                 | _  => let
   5.400 -                    val imp = S.list_mk_conj cntxt ==> P_y
   5.401 -                    val lvs = subtract (op aconv) globals (S.free_vars_lr imp)
   5.402 -                    val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs
   5.403 -                    in (S.list_mk_forall(locals,imp), (tm,locals)) end
   5.404 +                    val imp = USyntax.list_mk_conj cntxt ==> P_y
   5.405 +                    val lvs = subtract (op aconv) globals (USyntax.free_vars_lr imp)
   5.406 +                    val locals = #2(Utils.pluck (curry (op aconv) P) lvs) handle Utils.ERR _ => lvs
   5.407 +                    in (USyntax.list_mk_forall(locals,imp), (tm,locals)) end
   5.408           end
   5.409   in case TCs
   5.410 -    of [] => (S.list_mk_forall(pat_vars, P$pat), [])
   5.411 +    of [] => (USyntax.list_mk_forall(pat_vars, P$pat), [])
   5.412       |  _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
   5.413 -                 val ind_clause = S.list_mk_conj ihs ==> P$pat
   5.414 -             in (S.list_mk_forall(pat_vars,ind_clause), TCs_locals)
   5.415 +                 val ind_clause = USyntax.list_mk_conj ihs ==> P$pat
   5.416 +             in (USyntax.list_mk_forall(pat_vars,ind_clause), TCs_locals)
   5.417               end
   5.418   end
   5.419  end;
   5.420 @@ -776,29 +772,29 @@
   5.421   *---------------------------------------------------------------------------*)
   5.422  fun prove_case f thy (tm,TCs_locals,thm) =
   5.423   let val tych = Thry.typecheck thy
   5.424 -     val antc = tych(#ant(S.dest_imp tm))
   5.425 -     val thm' = R.SPEC_ALL thm
   5.426 -     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
   5.427 -     fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC)))))
   5.428 +     val antc = tych(#ant(USyntax.dest_imp tm))
   5.429 +     val thm' = Rules.SPEC_ALL thm
   5.430 +     fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
   5.431 +     fun get_cntxt TC = tych(#ant(USyntax.dest_imp(#2(USyntax.strip_forall(concl TC)))))
   5.432       fun mk_ih ((TC,locals),th2,nested) =
   5.433 -         R.GENL (map tych locals)
   5.434 -            (if nested then R.DISCH (get_cntxt TC) th2 handle U.ERR _ => th2
   5.435 -             else if S.is_imp (concl TC) then R.IMP_TRANS TC th2
   5.436 -             else R.MP th2 TC)
   5.437 +         Rules.GENL (map tych locals)
   5.438 +            (if nested then Rules.DISCH (get_cntxt TC) th2 handle Utils.ERR _ => th2
   5.439 +             else if USyntax.is_imp (concl TC) then Rules.IMP_TRANS TC th2
   5.440 +             else Rules.MP th2 TC)
   5.441   in
   5.442 - R.DISCH antc
   5.443 - (if S.is_imp(concl thm') (* recursive calls in this clause *)
   5.444 -  then let val th1 = R.ASSUME antc
   5.445 + Rules.DISCH antc
   5.446 + (if USyntax.is_imp(concl thm') (* recursive calls in this clause *)
   5.447 +  then let val th1 = Rules.ASSUME antc
   5.448             val TCs = map #1 TCs_locals
   5.449 -           val ylist = map (#2 o S.dest_relation o #2 o S.strip_imp o
   5.450 -                            #2 o S.strip_forall) TCs
   5.451 -           val TClist = map (fn(TC,lvs) => (R.SPEC_ALL(R.ASSUME(tych TC)),lvs))
   5.452 +           val ylist = map (#2 o USyntax.dest_relation o #2 o USyntax.strip_imp o
   5.453 +                            #2 o USyntax.strip_forall) TCs
   5.454 +           val TClist = map (fn(TC,lvs) => (Rules.SPEC_ALL(Rules.ASSUME(tych TC)),lvs))
   5.455                              TCs_locals
   5.456 -           val th2list = map (U.C R.SPEC th1 o tych) ylist
   5.457 +           val th2list = map (Utils.C Rules.SPEC th1 o tych) ylist
   5.458             val nlist = map nested TCs
   5.459 -           val triples = U.zip3 TClist th2list nlist
   5.460 +           val triples = Utils.zip3 TClist th2list nlist
   5.461             val Pylist = map mk_ih triples
   5.462 -       in R.MP thm' (R.LIST_CONJ Pylist) end
   5.463 +       in Rules.MP thm' (Rules.LIST_CONJ Pylist) end
   5.464    else thm')
   5.465   end;
   5.466  
   5.467 @@ -812,12 +808,12 @@
   5.468   *---------------------------------------------------------------------------*)
   5.469  fun LEFT_ABS_VSTRUCT tych thm =
   5.470    let fun CHOOSER v (tm,thm) =
   5.471 -        let val ex_tm = S.mk_exists{Bvar=v,Body=tm}
   5.472 -        in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm)
   5.473 +        let val ex_tm = USyntax.mk_exists{Bvar=v,Body=tm}
   5.474 +        in (ex_tm, Rules.CHOOSE(tych v, Rules.ASSUME (tych ex_tm)) thm)
   5.475          end
   5.476 -      val [veq] = filter (can S.dest_eq) (#1 (R.dest_thm thm))
   5.477 -      val {lhs,rhs} = S.dest_eq veq
   5.478 -      val L = S.free_vars_lr rhs
   5.479 +      val [veq] = filter (can USyntax.dest_eq) (#1 (Rules.dest_thm thm))
   5.480 +      val {lhs,rhs} = USyntax.dest_eq veq
   5.481 +      val L = USyntax.free_vars_lr rhs
   5.482    in  #2 (fold_rev CHOOSER L (veq,thm))  end;
   5.483  
   5.484  
   5.485 @@ -830,39 +826,39 @@
   5.486   *---------------------------------------------------------------------------*)
   5.487  fun mk_induction thy {fconst, R, SV, pat_TCs_list} =
   5.488  let val tych = Thry.typecheck thy
   5.489 -    val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM)
   5.490 +    val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) Thms.WF_INDUCTION_THM)
   5.491      val (pats,TCsl) = ListPair.unzip pat_TCs_list
   5.492      val case_thm = complete_cases thy pats
   5.493      val domain = (type_of o hd) pats
   5.494      val Pname = Name.variant (List.foldr (Library.foldr OldTerm.add_term_names)
   5.495                                [] (pats::TCsl)) "P"
   5.496      val P = Free(Pname, domain --> HOLogic.boolT)
   5.497 -    val Sinduct = R.SPEC (tych P) Sinduction
   5.498 -    val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
   5.499 +    val Sinduct = Rules.SPEC (tych P) Sinduction
   5.500 +    val Sinduct_assumf = USyntax.rand ((#ant o USyntax.dest_imp o concl) Sinduct)
   5.501      val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list
   5.502      val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
   5.503 -    val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
   5.504 +    val Rinduct_assum = Rules.ASSUME (tych (USyntax.list_mk_conj Rassums))
   5.505      val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
   5.506 -    val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
   5.507 +    val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
   5.508      val proved_cases = map (prove_case fconst thy) tasks
   5.509      val v = Free (Name.variant (List.foldr OldTerm.add_term_names [] (map concl proved_cases))
   5.510                      "v",
   5.511                    domain)
   5.512      val vtyped = tych v
   5.513 -    val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
   5.514 -    val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th')
   5.515 +    val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
   5.516 +    val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS[th]th')
   5.517                            (substs, proved_cases)
   5.518      val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1
   5.519 -    val dant = R.GEN vtyped (R.DISJ_CASESL (R.ISPEC vtyped case_thm) abs_cases)
   5.520 -    val dc = R.MP Sinduct dant
   5.521 -    val Parg_ty = type_of(#Bvar(S.dest_forall(concl dc)))
   5.522 -    val vars = map (gvvariant[Pname]) (S.strip_prod_type Parg_ty)
   5.523 -    val dc' = fold_rev (R.GEN o tych) vars
   5.524 -                       (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc)
   5.525 +    val dant = Rules.GEN vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
   5.526 +    val dc = Rules.MP Sinduct dant
   5.527 +    val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc)))
   5.528 +    val vars = map (gvvariant[Pname]) (USyntax.strip_prod_type Parg_ty)
   5.529 +    val dc' = fold_rev (Rules.GEN o tych) vars
   5.530 +                       (Rules.SPEC (tych(USyntax.mk_vstruct Parg_ty vars)) dc)
   5.531  in
   5.532 -   R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc')
   5.533 +   Rules.GEN (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc')
   5.534  end
   5.535 -handle U.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
   5.536 +handle Utils.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
   5.537  
   5.538  
   5.539  
   5.540 @@ -876,15 +872,15 @@
   5.541  
   5.542  fun simplify_induction thy hth ind =
   5.543    let val tych = Thry.typecheck thy
   5.544 -      val (asl,_) = R.dest_thm ind
   5.545 -      val (_,tc_eq_tc') = R.dest_thm hth
   5.546 -      val tc = S.lhs tc_eq_tc'
   5.547 +      val (asl,_) = Rules.dest_thm ind
   5.548 +      val (_,tc_eq_tc') = Rules.dest_thm hth
   5.549 +      val tc = USyntax.lhs tc_eq_tc'
   5.550        fun loop [] = ind
   5.551          | loop (asm::rst) =
   5.552            if (can (Thry.match_term thy asm) tc)
   5.553 -          then R.UNDISCH
   5.554 -                 (R.MATCH_MP
   5.555 -                     (R.MATCH_MP Thms.simp_thm (R.DISCH (tych asm) ind))
   5.556 +          then Rules.UNDISCH
   5.557 +                 (Rules.MATCH_MP
   5.558 +                     (Rules.MATCH_MP Thms.simp_thm (Rules.DISCH (tych asm) ind))
   5.559                       hth)
   5.560           else loop rst
   5.561    in loop asl
   5.562 @@ -896,7 +892,7 @@
   5.563   * assumption to the theorem.
   5.564   *---------------------------------------------------------------------------*)
   5.565  fun elim_tc tcthm (rule,induction) =
   5.566 -   (R.MP rule tcthm, R.PROVE_HYP tcthm induction)
   5.567 +   (Rules.MP rule tcthm, Rules.PROVE_HYP tcthm induction)
   5.568  
   5.569  
   5.570  fun trace_thms s L =
   5.571 @@ -911,17 +907,17 @@
   5.572  
   5.573  fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
   5.574  let val tych = Thry.typecheck theory
   5.575 -    val prove = R.prove strict;
   5.576 +    val prove = Rules.prove strict;
   5.577  
   5.578     (*---------------------------------------------------------------------
   5.579      * Attempt to eliminate WF condition. It's the only assumption of rules
   5.580      *---------------------------------------------------------------------*)
   5.581     val (rules1,induction1)  =
   5.582         let val thm = prove(tych(HOLogic.mk_Trueprop
   5.583 -                                  (hd(#1(R.dest_thm rules)))),
   5.584 +                                  (hd(#1(Rules.dest_thm rules)))),
   5.585                               wf_tac)
   5.586 -       in (R.PROVE_HYP thm rules,  R.PROVE_HYP thm induction)
   5.587 -       end handle U.ERR _ => (rules,induction);
   5.588 +       in (Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction)
   5.589 +       end handle Utils.ERR _ => (rules,induction);
   5.590  
   5.591     (*----------------------------------------------------------------------
   5.592      * The termination condition (tc) is simplified to |- tc = tc' (there
   5.593 @@ -938,14 +934,14 @@
   5.594             val tc_eq = simplifier tc1
   5.595             val _ = trace_thms "result: " [tc_eq]
   5.596         in
   5.597 -       elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
   5.598 -       handle U.ERR _ =>
   5.599 -        (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
   5.600 -                  (prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))),
   5.601 +       elim_tc (Rules.MATCH_MP Thms.eqT tc_eq) (r,ind)
   5.602 +       handle Utils.ERR _ =>
   5.603 +        (elim_tc (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq)
   5.604 +                  (prove(tych(HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq))),
   5.605                             terminator)))
   5.606                   (r,ind)
   5.607 -         handle U.ERR _ =>
   5.608 -          (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq),
   5.609 +         handle Utils.ERR _ =>
   5.610 +          (Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP Thms.simp_thm r) tc_eq),
   5.611             simplify_induction theory tc_eq ind))
   5.612         end
   5.613  
   5.614 @@ -963,35 +959,35 @@
   5.615      *   3. return |- tc = tc'
   5.616      *---------------------------------------------------------------------*)
   5.617     fun simplify_nested_tc tc =
   5.618 -      let val tc_eq = simplifier (tych (#2 (S.strip_forall tc)))
   5.619 +      let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc)))
   5.620        in
   5.621 -      R.GEN_ALL
   5.622 -       (R.MATCH_MP Thms.eqT tc_eq
   5.623 -        handle U.ERR _ =>
   5.624 -          (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
   5.625 -                      (prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))),
   5.626 +      Rules.GEN_ALL
   5.627 +       (Rules.MATCH_MP Thms.eqT tc_eq
   5.628 +        handle Utils.ERR _ =>
   5.629 +          (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq)
   5.630 +                      (prove(tych(HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq))),
   5.631                                 terminator))
   5.632 -            handle U.ERR _ => tc_eq))
   5.633 +            handle Utils.ERR _ => tc_eq))
   5.634        end
   5.635  
   5.636     (*-------------------------------------------------------------------
   5.637      * Attempt to simplify the termination conditions in each rule and
   5.638      * in the induction theorem.
   5.639      *-------------------------------------------------------------------*)
   5.640 -   fun strip_imp tm = if S.is_neg tm then ([],tm) else S.strip_imp tm
   5.641 +   fun strip_imp tm = if USyntax.is_neg tm then ([],tm) else USyntax.strip_imp tm
   5.642     fun loop ([],extras,R,ind) = (rev R, ind, extras)
   5.643       | loop ((r,ftcs)::rst, nthms, R, ind) =
   5.644          let val tcs = #1(strip_imp (concl r))
   5.645              val extra_tcs = subtract (op aconv) tcs ftcs
   5.646              val extra_tc_thms = map simplify_nested_tc extra_tcs
   5.647              val (r1,ind1) = fold simplify_tc tcs (r,ind)
   5.648 -            val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1
   5.649 +            val r2 = Rules.FILTER_DISCH_ALL(not o USyntax.is_WFR) r1
   5.650          in loop(rst, nthms@extra_tc_thms, r2::R, ind1)
   5.651          end
   5.652 -   val rules_tcs = ListPair.zip (R.CONJUNCTS rules1, TCs)
   5.653 +   val rules_tcs = ListPair.zip (Rules.CONJUNCTS rules1, TCs)
   5.654     val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1)
   5.655  in
   5.656 -  {induction = ind2, rules = R.LIST_CONJ rules2, nested_tcs = extras}
   5.657 +  {induction = ind2, rules = Rules.LIST_CONJ rules2, nested_tcs = extras}
   5.658  end;
   5.659  
   5.660  
     6.1 --- a/src/Tools/eqsubst.ML	Wed Dec 15 15:01:34 2010 +0100
     6.2 +++ b/src/Tools/eqsubst.ML	Wed Dec 15 15:11:56 2010 +0100
     6.3 @@ -119,11 +119,8 @@
     6.4  
     6.5  end;
     6.6  
     6.7 -structure EqSubst
     6.8 -: EQSUBST
     6.9 -= struct
    6.10 -
    6.11 -structure Z = Zipper;
    6.12 +structure EqSubst: EQSUBST =
    6.13 +struct
    6.14  
    6.15  (* changes object "=" to meta "==" which prepares a given rewrite rule *)
    6.16  fun prep_meta_eq ctxt =
    6.17 @@ -196,11 +193,11 @@
    6.18  abstracted out) for use in rewriting with RWInst.rw *)
    6.19  fun prep_zipper_match z = 
    6.20      let 
    6.21 -      val t = Z.trm z  
    6.22 -      val c = Z.ctxt z
    6.23 -      val Ts = Z.C.nty_ctxt c
    6.24 +      val t = Zipper.trm z  
    6.25 +      val c = Zipper.ctxt z
    6.26 +      val Ts = Zipper.C.nty_ctxt c
    6.27        val (FakeTs', Ts', t') = fakefree_badbounds Ts t
    6.28 -      val absterm = mk_foo_match (Z.C.apply c) Ts' t'
    6.29 +      val absterm = mk_foo_match (Zipper.C.apply c) Ts' t'
    6.30      in
    6.31        (t', (FakeTs', Ts', absterm))
    6.32      end;
    6.33 @@ -291,7 +288,7 @@
    6.34  (* Avoid considering replacing terms which have a var at the head as
    6.35     they always succeed trivially, and uninterestingly. *)
    6.36  fun valid_match_start z =
    6.37 -    (case bot_left_leaf_of (Z.trm z) of 
    6.38 +    (case bot_left_leaf_of (Zipper.trm z) of 
    6.39        Var _ => false 
    6.40        | _ => true);
    6.41  
    6.42 @@ -302,33 +299,33 @@
    6.43  fun search_lr_valid validf =
    6.44      let 
    6.45        fun sf_valid_td_lr z = 
    6.46 -          let val here = if validf z then [Z.Here z] else [] in
    6.47 -            case Z.trm z 
    6.48 -             of _ $ _ => [Z.LookIn (Z.move_down_left z)] 
    6.49 +          let val here = if validf z then [Zipper.Here z] else [] in
    6.50 +            case Zipper.trm z 
    6.51 +             of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z)] 
    6.52                           @ here 
    6.53 -                         @ [Z.LookIn (Z.move_down_right z)]
    6.54 -              | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)]
    6.55 +                         @ [Zipper.LookIn (Zipper.move_down_right z)]
    6.56 +              | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
    6.57                | _ => here
    6.58            end;
    6.59 -    in Z.lzy_search sf_valid_td_lr end;
    6.60 +    in Zipper.lzy_search sf_valid_td_lr end;
    6.61  
    6.62  (* search from bottom to top, left to right *)
    6.63  
    6.64  fun search_bt_valid validf =
    6.65      let 
    6.66        fun sf_valid_td_lr z = 
    6.67 -          let val here = if validf z then [Z.Here z] else [] in
    6.68 -            case Z.trm z 
    6.69 -             of _ $ _ => [Z.LookIn (Z.move_down_left z), 
    6.70 -                          Z.LookIn (Z.move_down_right z)] @ here
    6.71 -              | Abs _ => [Z.LookIn (Z.move_down_abs z)] @ here
    6.72 +          let val here = if validf z then [Zipper.Here z] else [] in
    6.73 +            case Zipper.trm z 
    6.74 +             of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z), 
    6.75 +                          Zipper.LookIn (Zipper.move_down_right z)] @ here
    6.76 +              | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
    6.77                | _ => here
    6.78            end;
    6.79 -    in Z.lzy_search sf_valid_td_lr end;
    6.80 +    in Zipper.lzy_search sf_valid_td_lr end;
    6.81  
    6.82  fun searchf_unify_gen f (sgn, maxidx, z) lhs =
    6.83      Seq.map (clean_unify_z sgn maxidx lhs) 
    6.84 -            (Z.limit_apply f z);
    6.85 +            (Zipper.limit_apply f z);
    6.86  
    6.87  (* search all unifications *)
    6.88  val searchf_lr_unify_all =
    6.89 @@ -369,9 +366,9 @@
    6.90        val conclterm = Logic.strip_imp_concl fixedbody;
    6.91        val conclthm = trivify conclterm;
    6.92        val maxidx = Thm.maxidx_of th;
    6.93 -      val ft = ((Z.move_down_right (* ==> *)
    6.94 -                 o Z.move_down_left (* Trueprop *)
    6.95 -                 o Z.mktop
    6.96 +      val ft = ((Zipper.move_down_right (* ==> *)
    6.97 +                 o Zipper.move_down_left (* Trueprop *)
    6.98 +                 o Zipper.mktop
    6.99                   o Thm.prop_of) conclthm)
   6.100      in
   6.101        ((cfvs, conclthm), (sgn, maxidx, ft))
   6.102 @@ -487,8 +484,8 @@
   6.103        val pth = trivify asmt;
   6.104        val maxidx = Thm.maxidx_of th;
   6.105  
   6.106 -      val ft = ((Z.move_down_right (* trueprop *)
   6.107 -                 o Z.mktop
   6.108 +      val ft = ((Zipper.move_down_right (* trueprop *)
   6.109 +                 o Zipper.mktop
   6.110                   o Thm.prop_of) pth)
   6.111      in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
   6.112