inserted tabs again
authorclasohm
Mon Jan 29 14:16:13 1996 +0100 (1996-01-29)
changeset 14605a6f2aabd538
parent 1459 d12da312eff4
child 1461 6bcb44e4d6e5
inserted tabs again
src/Pure/drule.ML
src/Pure/envir.ML
src/Pure/goals.ML
src/Pure/library.ML
src/Pure/logic.ML
src/Pure/net.ML
src/Pure/pattern.ML
src/Pure/section_utils.ML
src/Pure/sequence.ML
src/Pure/sign.ML
src/Pure/tactic.ML
src/Pure/tctical.ML
src/Pure/term.ML
src/Pure/thm.ML
src/Pure/type.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/drule.ML	Mon Jan 29 13:58:15 1996 +0100
     1.2 +++ b/src/Pure/drule.ML	Mon Jan 29 14:16:13 1996 +0100
     1.3 @@ -12,77 +12,77 @@
     1.4    sig
     1.5    structure Thm : THM
     1.6    local open Thm  in
     1.7 -  val add_defs          : (string * string) list -> theory -> theory
     1.8 -  val add_defs_i        : (string * term) list -> theory -> theory
     1.9 -  val asm_rl            : thm
    1.10 -  val assume_ax         : theory -> string -> thm
    1.11 -  val COMP              : thm * thm -> thm
    1.12 -  val compose           : thm * int * thm -> thm list
    1.13 -  val cprems_of         : thm -> cterm list
    1.14 -  val cskip_flexpairs   : cterm -> cterm
    1.15 -  val cstrip_imp_prems  : cterm -> cterm list
    1.16 -  val cterm_instantiate : (cterm*cterm)list -> thm -> thm
    1.17 -  val cut_rl            : thm
    1.18 -  val equal_abs_elim    : cterm  -> thm -> thm
    1.19 +  val add_defs		: (string * string) list -> theory -> theory
    1.20 +  val add_defs_i	: (string * term) list -> theory -> theory
    1.21 +  val asm_rl		: thm
    1.22 +  val assume_ax		: theory -> string -> thm
    1.23 +  val COMP		: thm * thm -> thm
    1.24 +  val compose		: thm * int * thm -> thm list
    1.25 +  val cprems_of		: thm -> cterm list
    1.26 +  val cskip_flexpairs	: cterm -> cterm
    1.27 +  val cstrip_imp_prems	: cterm -> cterm list
    1.28 +  val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
    1.29 +  val cut_rl		: thm
    1.30 +  val equal_abs_elim	: cterm  -> thm -> thm
    1.31    val equal_abs_elim_list: cterm list -> thm -> thm
    1.32 -  val eq_thm            : thm * thm -> bool
    1.33 -  val same_thm          : thm * thm -> bool
    1.34 -  val eq_thm_sg         : thm * thm -> bool
    1.35 +  val eq_thm		: thm * thm -> bool
    1.36 +  val same_thm		: thm * thm -> bool
    1.37 +  val eq_thm_sg		: thm * thm -> bool
    1.38    val flexpair_abs_elim_list: cterm list -> thm -> thm
    1.39 -  val forall_intr_list  : cterm list -> thm -> thm
    1.40 -  val forall_intr_frees : thm -> thm
    1.41 -  val forall_intr_vars  : thm -> thm
    1.42 -  val forall_elim_list  : cterm list -> thm -> thm
    1.43 -  val forall_elim_var   : int -> thm -> thm
    1.44 -  val forall_elim_vars  : int -> thm -> thm
    1.45 -  val implies_elim_list : thm -> thm list -> thm
    1.46 -  val implies_intr_list : cterm list -> thm -> thm
    1.47 -  val MRL               : thm list list * thm list -> thm list
    1.48 -  val MRS               : thm list * thm -> thm
    1.49 -  val pprint_cterm      : cterm -> pprint_args -> unit
    1.50 -  val pprint_ctyp       : ctyp -> pprint_args -> unit
    1.51 -  val pprint_theory     : theory -> pprint_args -> unit
    1.52 -  val pprint_thm        : thm -> pprint_args -> unit
    1.53 -  val pretty_thm        : thm -> Sign.Syntax.Pretty.T
    1.54 -  val print_cterm       : cterm -> unit
    1.55 -  val print_ctyp        : ctyp -> unit
    1.56 -  val print_goals       : int -> thm -> unit
    1.57 -  val print_goals_ref   : (int -> thm -> unit) ref
    1.58 -  val print_syntax      : theory -> unit
    1.59 -  val print_theory      : theory -> unit
    1.60 -  val print_thm         : thm -> unit
    1.61 -  val prth              : thm -> thm
    1.62 -  val prthq             : thm Sequence.seq -> thm Sequence.seq
    1.63 -  val prths             : thm list -> thm list
    1.64 -  val read_instantiate  : (string*string)list -> thm -> thm
    1.65 +  val forall_intr_list	: cterm list -> thm -> thm
    1.66 +  val forall_intr_frees	: thm -> thm
    1.67 +  val forall_intr_vars	: thm -> thm
    1.68 +  val forall_elim_list	: cterm list -> thm -> thm
    1.69 +  val forall_elim_var	: int -> thm -> thm
    1.70 +  val forall_elim_vars	: int -> thm -> thm
    1.71 +  val implies_elim_list	: thm -> thm list -> thm
    1.72 +  val implies_intr_list	: cterm list -> thm -> thm
    1.73 +  val MRL		: thm list list * thm list -> thm list
    1.74 +  val MRS		: thm list * thm -> thm
    1.75 +  val pprint_cterm	: cterm -> pprint_args -> unit
    1.76 +  val pprint_ctyp	: ctyp -> pprint_args -> unit
    1.77 +  val pprint_theory	: theory -> pprint_args -> unit
    1.78 +  val pprint_thm	: thm -> pprint_args -> unit
    1.79 +  val pretty_thm	: thm -> Sign.Syntax.Pretty.T
    1.80 +  val print_cterm	: cterm -> unit
    1.81 +  val print_ctyp	: ctyp -> unit
    1.82 +  val print_goals	: int -> thm -> unit
    1.83 +  val print_goals_ref	: (int -> thm -> unit) ref
    1.84 +  val print_syntax	: theory -> unit
    1.85 +  val print_theory	: theory -> unit
    1.86 +  val print_thm		: thm -> unit
    1.87 +  val prth		: thm -> thm
    1.88 +  val prthq		: thm Sequence.seq -> thm Sequence.seq
    1.89 +  val prths		: thm list -> thm list
    1.90 +  val read_instantiate	: (string*string)list -> thm -> thm
    1.91    val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
    1.92 -  val read_insts        :
    1.93 +  val read_insts	:
    1.94            Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
    1.95                    -> (indexname -> typ option) * (indexname -> sort option)
    1.96                    -> string list -> (string*string)list
    1.97                    -> (indexname*ctyp)list * (cterm*cterm)list
    1.98 -  val reflexive_thm     : thm
    1.99 -  val revcut_rl         : thm
   1.100 -  val rewrite_goal_rule : bool*bool -> (meta_simpset -> thm -> thm option)
   1.101 +  val reflexive_thm	: thm
   1.102 +  val revcut_rl		: thm
   1.103 +  val rewrite_goal_rule	: bool*bool -> (meta_simpset -> thm -> thm option)
   1.104          -> meta_simpset -> int -> thm -> thm
   1.105    val rewrite_goals_rule: thm list -> thm -> thm
   1.106 -  val rewrite_rule      : thm list -> thm -> thm
   1.107 -  val RS                : thm * thm -> thm
   1.108 -  val RSN               : thm * (int * thm) -> thm
   1.109 -  val RL                : thm list * thm list -> thm list
   1.110 -  val RLN               : thm list * (int * thm list) -> thm list
   1.111 -  val show_hyps         : bool ref
   1.112 -  val size_of_thm       : thm -> int
   1.113 -  val standard          : thm -> thm
   1.114 -  val string_of_cterm   : cterm -> string
   1.115 -  val string_of_ctyp    : ctyp -> string
   1.116 -  val string_of_thm     : thm -> string
   1.117 -  val symmetric_thm     : thm
   1.118 -  val thin_rl           : thm
   1.119 -  val transitive_thm    : thm
   1.120 +  val rewrite_rule	: thm list -> thm -> thm
   1.121 +  val RS		: thm * thm -> thm
   1.122 +  val RSN		: thm * (int * thm) -> thm
   1.123 +  val RL		: thm list * thm list -> thm list
   1.124 +  val RLN		: thm list * (int * thm list) -> thm list
   1.125 +  val show_hyps		: bool ref
   1.126 +  val size_of_thm	: thm -> int
   1.127 +  val standard		: thm -> thm
   1.128 +  val string_of_cterm	: cterm -> string
   1.129 +  val string_of_ctyp	: ctyp -> string
   1.130 +  val string_of_thm	: thm -> string
   1.131 +  val symmetric_thm	: thm
   1.132 +  val thin_rl		: thm
   1.133 +  val transitive_thm	: thm
   1.134    val triv_forall_equality: thm
   1.135    val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
   1.136 -  val zero_var_indexes  : thm -> thm
   1.137 +  val zero_var_indexes	: thm -> thm
   1.138    end
   1.139    end;
   1.140  
   1.141 @@ -226,8 +226,8 @@
   1.142  (*Discard flexflex pairs; return a cterm*)
   1.143  fun cskip_flexpairs ct =
   1.144      case term_of ct of
   1.145 -        (Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
   1.146 -            cskip_flexpairs (#2 (dest_cimplies ct))
   1.147 +	(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
   1.148 +	    cskip_flexpairs (#2 (dest_cimplies ct))
   1.149        | _ => ct;
   1.150  
   1.151  (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   1.152 @@ -732,15 +732,15 @@
   1.153  (*Rewrite a theorem*)
   1.154  fun rewrite_rule []   th = th
   1.155    | rewrite_rule thms th =
   1.156 -        fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms)) th;
   1.157 +	fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms)) th;
   1.158  
   1.159  (*Rewrite the subgoals of a proof state (represented by a theorem) *)
   1.160  fun rewrite_goals_rule []   th = th
   1.161    | rewrite_goals_rule thms th =
   1.162 -        fconv_rule (goals_conv (K true) 
   1.163 -                    (rew_conv (true,false) (K(K None))
   1.164 -                     (Thm.mss_of thms))) 
   1.165 -                   th;
   1.166 +	fconv_rule (goals_conv (K true) 
   1.167 +		    (rew_conv (true,false) (K(K None))
   1.168 +		     (Thm.mss_of thms))) 
   1.169 +	           th;
   1.170  
   1.171  (*Rewrite the subgoal of a proof state (represented by a theorem) *)
   1.172  fun rewrite_goal_rule mode prover mss i thm =
     2.1 --- a/src/Pure/envir.ML	Mon Jan 29 13:58:15 1996 +0100
     2.2 +++ b/src/Pure/envir.ML	Mon Jan 29 14:16:13 1996 +0100
     2.3 @@ -18,19 +18,19 @@
     2.4    datatype env = Envir of {asol: term xolist,
     2.5                             iTs: (indexname * typ) list,
     2.6                             maxidx: int}
     2.7 -  val alist_of          : env -> (indexname * term) list
     2.8 -  val alist_of_olist    : 'a xolist -> (indexname * 'a) list
     2.9 -  val empty             : int->env
    2.10 -  val is_empty          : env -> bool
    2.11 -  val minidx            : env -> int option
    2.12 -  val genvar            : string -> env * typ -> env * term
    2.13 -  val genvars           : string -> env * typ list -> env * term list
    2.14 -  val lookup            : env * indexname -> term option
    2.15 -  val norm_term         : env -> term -> term
    2.16 -  val null_olist        : 'a xolist
    2.17 -  val olist_of_alist    : (indexname * 'a) list -> 'a xolist
    2.18 -  val update            : (indexname * term) * env -> env
    2.19 -  val vupdate           : (indexname * term) * env -> env
    2.20 +  val alist_of		: env -> (indexname * term) list
    2.21 +  val alist_of_olist	: 'a xolist -> (indexname * 'a) list
    2.22 +  val empty		: int->env
    2.23 +  val is_empty		: env -> bool
    2.24 +  val minidx		: env -> int option
    2.25 +  val genvar		: string -> env * typ -> env * term
    2.26 +  val genvars		: string -> env * typ list -> env * term list
    2.27 +  val lookup		: env * indexname -> term option
    2.28 +  val norm_term		: env -> term -> term
    2.29 +  val null_olist	: 'a xolist
    2.30 +  val olist_of_alist	: (indexname * 'a) list -> 'a xolist
    2.31 +  val update		: (indexname * term) * env -> env
    2.32 +  val vupdate		: (indexname * term) * env -> env
    2.33  end;
    2.34  
    2.35  functor EnvirFun () : ENVIR =
     3.1 --- a/src/Pure/goals.ML	Mon Jan 29 13:58:15 1996 +0100
     3.2 +++ b/src/Pure/goals.ML	Mon Jan 29 14:16:13 1996 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4 -(*  Title:      Pure/goals.ML
     3.5 +(*  Title: 	Pure/goals.ML
     3.6      ID:         $Id$
     3.7 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.8 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3.9      Copyright   1993  University of Cambridge
    3.10  
    3.11  Goal stack package.  The goal stack initially holds a dummy proof, and can
    3.12 @@ -15,63 +15,63 @@
    3.13    structure Tactical: TACTICAL
    3.14    local open Tactical Tactical.Thm in
    3.15    type proof
    3.16 -  val ba                : int -> unit
    3.17 -  val back              : unit -> unit
    3.18 -  val bd                : thm -> int -> unit
    3.19 -  val bds               : thm list -> int -> unit
    3.20 -  val be                : thm -> int -> unit
    3.21 -  val bes               : thm list -> int -> unit
    3.22 -  val br                : thm -> int -> unit
    3.23 -  val brs               : thm list -> int -> unit
    3.24 -  val bw                : thm -> unit
    3.25 -  val bws               : thm list -> unit
    3.26 -  val by                : tactic -> unit
    3.27 -  val byev              : tactic list -> unit
    3.28 -  val chop              : unit -> unit
    3.29 -  val choplev           : int -> unit
    3.30 -  val fa                : unit -> unit
    3.31 -  val fd                : thm -> unit
    3.32 -  val fds               : thm list -> unit
    3.33 -  val fe                : thm -> unit
    3.34 -  val fes               : thm list -> unit
    3.35 -  val filter_goal       : (term*term->bool) -> thm list -> int -> thm list
    3.36 -  val fr                : thm -> unit
    3.37 -  val frs               : thm list -> unit
    3.38 -  val getgoal           : int -> term
    3.39 -  val gethyps           : int -> thm list
    3.40 -  val goal              : theory -> string -> thm list
    3.41 -  val goalw             : theory -> thm list -> string -> thm list
    3.42 -  val goalw_cterm       : thm list -> cterm -> thm list
    3.43 -  val pop_proof         : unit -> thm list
    3.44 -  val pr                : unit -> unit
    3.45 -  val premises          : unit -> thm list
    3.46 -  val prin              : term -> unit
    3.47 -  val printyp           : typ -> unit
    3.48 -  val pprint_term       : term -> pprint_args -> unit
    3.49 -  val pprint_typ        : typ -> pprint_args -> unit
    3.50 -  val print_exn         : exn -> 'a
    3.51 -  val print_sign_exn    : Sign.sg -> exn -> 'a
    3.52 -  val prlev             : int -> unit
    3.53 -  val proof_timing      : bool ref
    3.54 -  val prove_goal        : theory -> string -> (thm list -> tactic list) -> thm
    3.55 +  val ba		: int -> unit
    3.56 +  val back		: unit -> unit
    3.57 +  val bd		: thm -> int -> unit
    3.58 +  val bds		: thm list -> int -> unit
    3.59 +  val be		: thm -> int -> unit
    3.60 +  val bes		: thm list -> int -> unit
    3.61 +  val br		: thm -> int -> unit
    3.62 +  val brs		: thm list -> int -> unit
    3.63 +  val bw		: thm -> unit
    3.64 +  val bws		: thm list -> unit
    3.65 +  val by		: tactic -> unit
    3.66 +  val byev		: tactic list -> unit
    3.67 +  val chop		: unit -> unit
    3.68 +  val choplev		: int -> unit
    3.69 +  val fa		: unit -> unit
    3.70 +  val fd		: thm -> unit
    3.71 +  val fds		: thm list -> unit
    3.72 +  val fe		: thm -> unit
    3.73 +  val fes		: thm list -> unit
    3.74 +  val filter_goal	: (term*term->bool) -> thm list -> int -> thm list
    3.75 +  val fr		: thm -> unit
    3.76 +  val frs		: thm list -> unit
    3.77 +  val getgoal		: int -> term
    3.78 +  val gethyps		: int -> thm list
    3.79 +  val goal		: theory -> string -> thm list
    3.80 +  val goalw		: theory -> thm list -> string -> thm list
    3.81 +  val goalw_cterm	: thm list -> cterm -> thm list
    3.82 +  val pop_proof		: unit -> thm list
    3.83 +  val pr		: unit -> unit
    3.84 +  val premises		: unit -> thm list
    3.85 +  val prin		: term -> unit
    3.86 +  val printyp		: typ -> unit
    3.87 +  val pprint_term	: term -> pprint_args -> unit
    3.88 +  val pprint_typ	: typ -> pprint_args -> unit
    3.89 +  val print_exn		: exn -> 'a
    3.90 +  val print_sign_exn	: Sign.sg -> exn -> 'a
    3.91 +  val prlev		: int -> unit
    3.92 +  val proof_timing	: bool ref
    3.93 +  val prove_goal	: theory -> string -> (thm list -> tactic list) -> thm
    3.94    val prove_goalw      : theory->thm list->string->(thm list->tactic list)->thm
    3.95 -  val prove_goalw_cterm : thm list->cterm->(thm list->tactic list)->thm
    3.96 -  val push_proof        : unit -> unit
    3.97 -  val read              : string -> term
    3.98 -  val ren               : string -> int -> unit
    3.99 -  val restore_proof     : proof -> thm list
   3.100 -  val result            : unit -> thm  
   3.101 -  val rotate_proof      : unit -> thm list
   3.102 -  val uresult           : unit -> thm  
   3.103 -  val save_proof        : unit -> proof
   3.104 -  val topthm            : unit -> thm
   3.105 -  val undo              : unit -> unit
   3.106 +  val prove_goalw_cterm	: thm list->cterm->(thm list->tactic list)->thm
   3.107 +  val push_proof	: unit -> unit
   3.108 +  val read		: string -> term
   3.109 +  val ren		: string -> int -> unit
   3.110 +  val restore_proof	: proof -> thm list
   3.111 +  val result		: unit -> thm  
   3.112 +  val rotate_proof	: unit -> thm list
   3.113 +  val uresult		: unit -> thm  
   3.114 +  val save_proof	: unit -> proof
   3.115 +  val topthm		: unit -> thm
   3.116 +  val undo		: unit -> unit
   3.117    end
   3.118    end;
   3.119  
   3.120  functor GoalsFun (structure Logic: LOGIC and Drule: DRULE and Tactic: TACTIC
   3.121                          and Pattern:PATTERN
   3.122 -          sharing type Pattern.type_sig = Drule.Thm.Sign.Type.type_sig
   3.123 +	  sharing type Pattern.type_sig = Drule.Thm.Sign.Type.type_sig
   3.124                and Drule.Thm = Tactic.Tactical.Thm) : GOALS =
   3.125  struct
   3.126  structure Tactical = Tactic.Tactical
   3.127 @@ -132,39 +132,39 @@
   3.128        and st0 = (rewrite_goals_rule rths o trivial) (cterm_of sign B)
   3.129        fun result_error state msg = 
   3.130          (writeln ("Bad final proof state:");
   3.131 -         !print_goals_ref (!goals_limit) state;
   3.132 -         error msg)
   3.133 + 	 !print_goals_ref (!goals_limit) state;
   3.134 +	 error msg)
   3.135        (*discharges assumptions from state in the order they appear in goal;
   3.136 -        checks (if requested) that resulting theorem is equivalent to goal. *)
   3.137 +	checks (if requested) that resulting theorem is equivalent to goal. *)
   3.138        fun mkresult (check,state) =
   3.139          let val state = Sequence.hd (flexflex_rule state)
   3.140 -                        handle _ => state   (*smash flexflex pairs*)
   3.141 -            val ngoals = nprems_of state
   3.142 +	    		handle _ => state   (*smash flexflex pairs*)
   3.143 +	    val ngoals = nprems_of state
   3.144              val th = strip_shyps (implies_intr_list cAs state)
   3.145              val {hyps,prop,sign=sign',...} = rep_thm th
   3.146              val xshyps = extra_shyps th;
   3.147          in  if not check then standard th
   3.148 -            else if not (Sign.eq_sg(sign,sign')) then result_error state
   3.149 -                ("Signature of proof state has changed!" ^
   3.150 -                 sign_error (sign,sign'))
   3.151 +	    else if not (Sign.eq_sg(sign,sign')) then result_error state
   3.152 +		("Signature of proof state has changed!" ^
   3.153 +		 sign_error (sign,sign'))
   3.154              else if ngoals>0 then result_error state
   3.155 -                (string_of_int ngoals ^ " unsolved goals!")
   3.156 +		(string_of_int ngoals ^ " unsolved goals!")
   3.157              else if not (null hyps) then result_error state
   3.158                  ("Additional hypotheses:\n" ^ 
   3.159                   cat_lines (map (Sign.string_of_term sign) hyps))
   3.160 -            else if not (null xshyps) then result_error state
   3.161 +	    else if not (null xshyps) then result_error state
   3.162                  ("Extra sort hypotheses: " ^
   3.163                   commas (map Sign.Type.str_of_sort xshyps))
   3.164 -            else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
   3.165 -                                    (term_of chorn, prop)
   3.166 -                 then  standard th 
   3.167 -            else  result_error state "proved a different theorem"
   3.168 +	    else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
   3.169 +			            (term_of chorn, prop)
   3.170 +		 then  standard th 
   3.171 +	    else  result_error state "proved a different theorem"
   3.172          end
   3.173    in
   3.174       if Sign.eq_sg(sign, #sign(rep_thm st0))
   3.175       then (prems, st0, mkresult)
   3.176       else error ("Definitions would change the proof state's signature" ^
   3.177 -                 sign_error (sign, #sign(rep_thm st0)))
   3.178 +		 sign_error (sign, #sign(rep_thm st0)))
   3.179    end
   3.180    handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s);
   3.181  
   3.182 @@ -172,18 +172,18 @@
   3.183  fun print_sign_exn_unit sign e = 
   3.184    case e of
   3.185       THM (msg,i,thms) =>
   3.186 -         (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
   3.187 -          seq print_thm thms)
   3.188 +	 (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
   3.189 +	  seq print_thm thms)
   3.190     | THEORY (msg,thys) =>
   3.191 -         (writeln ("Exception THEORY raised:\n" ^ msg);
   3.192 -          seq print_theory thys)
   3.193 +	 (writeln ("Exception THEORY raised:\n" ^ msg);
   3.194 +	  seq print_theory thys)
   3.195     | TERM (msg,ts) =>
   3.196 -         (writeln ("Exception TERM raised:\n" ^ msg);
   3.197 -          seq (writeln o Sign.string_of_term sign) ts)
   3.198 +	 (writeln ("Exception TERM raised:\n" ^ msg);
   3.199 +	  seq (writeln o Sign.string_of_term sign) ts)
   3.200     | TYPE (msg,Ts,ts) =>
   3.201 -         (writeln ("Exception TYPE raised:\n" ^ msg);
   3.202 -          seq (writeln o Sign.string_of_typ sign) Ts;
   3.203 -          seq (writeln o Sign.string_of_term sign) ts)
   3.204 +	 (writeln ("Exception TYPE raised:\n" ^ msg);
   3.205 +	  seq (writeln o Sign.string_of_typ sign) Ts;
   3.206 +	  seq (writeln o Sign.string_of_term sign) ts)
   3.207     | e => raise e;
   3.208  
   3.209  (*Prints an exception, then fails*)
   3.210 @@ -199,13 +199,13 @@
   3.211    let val (prems, st0, mkresult) = prepare_proof rths chorn
   3.212        val tac = EVERY (tacsf prems)
   3.213        fun statef() = 
   3.214 -          (case Sequence.pull (tapply(tac,st0)) of 
   3.215 -               Some(st,_) => st
   3.216 -             | _ => error ("prove_goal: tactic failed"))
   3.217 +	  (case Sequence.pull (tapply(tac,st0)) of 
   3.218 +	       Some(st,_) => st
   3.219 +	     | _ => error ("prove_goal: tactic failed"))
   3.220    in  mkresult (true, cond_timeit (!proof_timing) statef)  end
   3.221    handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
   3.222 -               error ("The exception above was raised for\n" ^ 
   3.223 -                      string_of_cterm chorn));
   3.224 +	       error ("The exception above was raised for\n" ^ 
   3.225 +		      string_of_cterm chorn));
   3.226  
   3.227  
   3.228  (*Version taking the goal as a string*)
   3.229 @@ -214,7 +214,7 @@
   3.230        val chorn = read_cterm sign (agoal,propT)
   3.231    in  prove_goalw_cterm rths chorn tacsf end
   3.232    handle ERROR => error (*from read_cterm?*)
   3.233 -                ("The error above occurred for " ^ quote agoal);
   3.234 +		("The error above occurred for " ^ quote agoal);
   3.235  
   3.236  (*String version with no meta-rewrite-rules*)
   3.237  fun prove_goal thy = prove_goalw thy [];
   3.238 @@ -262,8 +262,8 @@
   3.239  (*Get subgoal i from goal stack*)
   3.240  fun getgoal i = 
   3.241        (case  drop (i-1, prems_of (topthm()))  of
   3.242 -            [] => error"getgoal: Goal number out of range"
   3.243 -          | Q::_ => Q);
   3.244 +	    [] => error"getgoal: Goal number out of range"
   3.245 +	  | Q::_ => Q);
   3.246  
   3.247  (*Return subgoal i's hypotheses as meta-level assumptions.
   3.248    For debugging uses of METAHYPS*)
   3.249 @@ -283,7 +283,7 @@
   3.250    in  if 0<=n andalso n<= level
   3.251        then  drop (level - n, pair::pairs) 
   3.252        else  error ("Level number must lie between 0 and " ^ 
   3.253 -                   string_of_int level)
   3.254 +		   string_of_int level)
   3.255    end;
   3.256  
   3.257  (*Print the given level of the proof*)
   3.258 @@ -309,7 +309,7 @@
   3.259  fun goalw thy rths agoal = 
   3.260    goalw_cterm rths (read_cterm(sign_of thy)(agoal,propT))
   3.261    handle ERROR => error (*from type_assign, etc via prepare_proof*)
   3.262 -            ("The error above occurred for " ^ quote agoal);
   3.263 +	    ("The error above occurred for " ^ quote agoal);
   3.264  
   3.265  (*String version with no meta-rewrite-rules*)
   3.266  fun goal thy = goalw thy [];
   3.267 @@ -320,10 +320,10 @@
   3.268       None      => error"by: tactic failed"
   3.269     | Some(th2,ths2) => 
   3.270         (if eq_thm(th,th2) 
   3.271 -          then writeln"Warning: same as previous level"
   3.272 -          else if eq_thm_sg(th,th2) then ()
   3.273 -          else writeln("Warning: signature of proof state has changed" ^
   3.274 -                       sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
   3.275 +	  then writeln"Warning: same as previous level"
   3.276 +	  else if eq_thm_sg(th,th2) then ()
   3.277 +	  else writeln("Warning: signature of proof state has changed" ^
   3.278 +		       sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
   3.279         ((th2,ths2)::(th,ths)::pairs)));
   3.280  
   3.281  fun by tac = cond_timeit (!proof_timing) 
   3.282 @@ -339,13 +339,13 @@
   3.283  fun backtrack [] = error"back: no alternatives"
   3.284    | backtrack ((th,thstr) :: pairs) =
   3.285       (case Sequence.pull thstr of
   3.286 -          None      => (writeln"Going back a level..."; backtrack pairs)
   3.287 -        | Some(th2,thstr2) =>  
   3.288 -           (if eq_thm(th,th2) 
   3.289 -              then writeln"Warning: same as previous choice at this level"
   3.290 -              else if eq_thm_sg(th,th2) then ()
   3.291 -              else writeln"Warning: signature of proof state has changed";
   3.292 -            (th2,thstr2)::pairs));
   3.293 +	  None      => (writeln"Going back a level..."; backtrack pairs)
   3.294 +	| Some(th2,thstr2) =>  
   3.295 +	   (if eq_thm(th,th2) 
   3.296 +	      then writeln"Warning: same as previous choice at this level"
   3.297 +	      else if eq_thm_sg(th,th2) then ()
   3.298 +	      else writeln"Warning: signature of proof state has changed";
   3.299 +	    (th2,thstr2)::pairs));
   3.300  
   3.301  fun back() = setstate (backtrack (getstate()));
   3.302  
   3.303 @@ -371,7 +371,7 @@
   3.304  
   3.305  
   3.306  fun top_proof() = case !proofstack of
   3.307 -        [] => error("Stack of proof attempts is empty!")
   3.308 +	[] => error("Stack of proof attempts is empty!")
   3.309      | p::ps => (p,ps);
   3.310  
   3.311  (*  push a copy of the current proof state on to the stack *)
   3.312 @@ -385,11 +385,11 @@
   3.313  
   3.314  (* rotate the stack so that the top element goes to the bottom *)
   3.315  fun rotate_proof() = let val (p,ps) = top_proof()
   3.316 -                    in proofstack := ps@[save_proof()];
   3.317 -                       restore_proof p;
   3.318 -                       pr();
   3.319 -                       !curr_prems
   3.320 -                    end;
   3.321 +		    in proofstack := ps@[save_proof()];
   3.322 +		       restore_proof p;
   3.323 +		       pr();
   3.324 +		       !curr_prems
   3.325 +		    end;
   3.326  
   3.327  
   3.328  (** Shortcuts for commonly-used tactics **)
   3.329 @@ -428,7 +428,7 @@
   3.330  fun top_sg() = #sign(rep_thm(topthm()));
   3.331  
   3.332  fun read s = term_of (read_cterm (top_sg())
   3.333 -                                           (s, (TVar(("DUMMY",0),[]))));
   3.334 +			                   (s, (TVar(("DUMMY",0),[]))));
   3.335  
   3.336  (*Print a term under the current signature of the proof state*)
   3.337  fun prin t = writeln (Sign.string_of_term (top_sg()) t);
     4.1 --- a/src/Pure/library.ML	Mon Jan 29 13:58:15 1996 +0100
     4.2 +++ b/src/Pure/library.ML	Mon Jan 29 14:16:13 1996 +0100
     4.3 @@ -650,8 +650,8 @@
     4.4  (*Assert pred for every member of l, generating a message if pred fails*)
     4.5  fun assert_all pred l msg_fn = 
     4.6    let fun asl [] = ()
     4.7 -        | asl (x::xs) = if pred x then asl xs
     4.8 -                        else error (msg_fn x)
     4.9 +	| asl (x::xs) = if pred x then asl xs
    4.10 +	                else error (msg_fn x)
    4.11    in  asl l  end;
    4.12  
    4.13  (* FIXME close file (?) *)
     5.1 --- a/src/Pure/logic.ML	Mon Jan 29 13:58:15 1996 +0100
     5.2 +++ b/src/Pure/logic.ML	Mon Jan 29 14:16:13 1996 +0100
     5.3 @@ -1,6 +1,6 @@
     5.4 -(*  Title:      Pure/logic.ML
     5.5 +(*  Title: 	Pure/logic.ML
     5.6      ID:         $Id$
     5.7 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.8 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     5.9      Copyright   Cambridge University 1992
    5.10  
    5.11  Supporting code for defining the abstract type "thm"
    5.12 @@ -10,43 +10,43 @@
    5.13  
    5.14  signature LOGIC = 
    5.15    sig
    5.16 -  val assum_pairs       : term -> (term*term)list
    5.17 -  val auto_rename       : bool ref   
    5.18 -  val close_form        : term -> term   
    5.19 -  val count_prems       : term * int -> int
    5.20 -  val dest_equals       : term -> term * term
    5.21 -  val dest_flexpair     : term -> term * term
    5.22 -  val dest_implies      : term -> term * term
    5.23 -  val dest_inclass      : term -> typ * class
    5.24 -  val dest_type         : term -> typ
    5.25 -  val flatten_params    : int -> term -> term
    5.26 -  val freeze_vars       : term -> term
    5.27 -  val incr_indexes      : typ list * int -> term -> term
    5.28 -  val lift_fns          : term * int -> (term -> term) * (term -> term)
    5.29 -  val list_flexpairs    : (term*term)list * term -> term
    5.30 -  val list_implies      : term list * term -> term
    5.31 +  val assum_pairs	: term -> (term*term)list
    5.32 +  val auto_rename	: bool ref   
    5.33 +  val close_form	: term -> term   
    5.34 +  val count_prems	: term * int -> int
    5.35 +  val dest_equals	: term -> term * term
    5.36 +  val dest_flexpair	: term -> term * term
    5.37 +  val dest_implies	: term -> term * term
    5.38 +  val dest_inclass	: term -> typ * class
    5.39 +  val dest_type		: term -> typ
    5.40 +  val flatten_params	: int -> term -> term
    5.41 +  val freeze_vars	: term -> term
    5.42 +  val incr_indexes	: typ list * int -> term -> term
    5.43 +  val lift_fns		: term * int -> (term -> term) * (term -> term)
    5.44 +  val list_flexpairs	: (term*term)list * term -> term
    5.45 +  val list_implies	: term list * term -> term
    5.46    val list_rename_params: string list * term -> term
    5.47    val is_equals         : term -> bool
    5.48 -  val mk_equals         : term * term -> term
    5.49 -  val mk_flexpair       : term * term -> term
    5.50 -  val mk_implies        : term * term -> term
    5.51 -  val mk_inclass        : typ * class -> term
    5.52 -  val mk_type           : typ -> term
    5.53 -  val occs              : term * term -> bool
    5.54 -  val rule_of           : (term*term)list * term list * term -> term
    5.55 -  val set_rename_prefix : string -> unit   
    5.56 -  val skip_flexpairs    : term -> term
    5.57 +  val mk_equals		: term * term -> term
    5.58 +  val mk_flexpair	: term * term -> term
    5.59 +  val mk_implies	: term * term -> term
    5.60 +  val mk_inclass	: typ * class -> term
    5.61 +  val mk_type		: typ -> term
    5.62 +  val occs		: term * term -> bool
    5.63 +  val rule_of		: (term*term)list * term list * term -> term
    5.64 +  val set_rename_prefix	: string -> unit   
    5.65 +  val skip_flexpairs	: term -> term
    5.66    val strip_assums_concl: term -> term
    5.67 -  val strip_assums_hyp  : term -> term list
    5.68 -  val strip_flexpairs   : term -> (term*term)list * term
    5.69 -  val strip_horn        : term -> (term*term)list * term list * term
    5.70 -  val strip_imp_concl   : term -> term
    5.71 -  val strip_imp_prems   : term -> term list
    5.72 -  val strip_params      : term -> (string * typ) list
    5.73 -  val strip_prems       : int * term list * term -> term list * term
    5.74 -  val thaw_vars         : term -> term
    5.75 -  val unvarify          : term -> term  
    5.76 -  val varify            : term -> term  
    5.77 +  val strip_assums_hyp	: term -> term list
    5.78 +  val strip_flexpairs	: term -> (term*term)list * term
    5.79 +  val strip_horn	: term -> (term*term)list * term list * term
    5.80 +  val strip_imp_concl	: term -> term
    5.81 +  val strip_imp_prems	: term -> term list
    5.82 +  val strip_params	: term -> (string * typ) list
    5.83 +  val strip_prems	: int * term list * term -> term list * term
    5.84 +  val thaw_vars		: term -> term
    5.85 +  val unvarify		: term -> term  
    5.86 +  val varify		: term -> term  
    5.87    end;
    5.88  
    5.89  functor LogicFun (structure Unify: UNIFY and Net:NET): LOGIC =
    5.90 @@ -91,11 +91,11 @@
    5.91    | strip_imp_concl A = A : term;
    5.92  
    5.93  (*Strip and return premises: (i, [], A1==>...Ai==>B)
    5.94 -    goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED) 
    5.95 +    goes to   ([Ai, A(i-1),...,A1] , B) 	(REVERSED) 
    5.96    if  i<0 or else i too big then raises  TERM*)
    5.97  fun strip_prems (0, As, B) = (As, B) 
    5.98    | strip_prems (i, As, Const("==>", _) $ A $ B) = 
    5.99 -        strip_prems (i-1, A::As, B)
   5.100 +	strip_prems (i-1, A::As, B)
   5.101    | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
   5.102  
   5.103  (*Count premises -- quicker than (length ostrip_prems) *)
   5.104 @@ -114,13 +114,13 @@
   5.105      goes to (a1=?=b1) ==>...(an=?=bn)==>C *)
   5.106  fun list_flexpairs ([], A) = A
   5.107    | list_flexpairs ((t,u)::pairs, A) =
   5.108 -        implies $ (mk_flexpair(t,u)) $ list_flexpairs(pairs,A);
   5.109 +	implies $ (mk_flexpair(t,u)) $ list_flexpairs(pairs,A);
   5.110  
   5.111  (*Make the object-rule tpairs==>As==>B   *)
   5.112  fun rule_of (tpairs, As, B) = list_flexpairs(tpairs, list_implies(As, B));
   5.113  
   5.114  (*Remove and return flexflex pairs: 
   5.115 -    (a1=?=b1)==>...(an=?=bn)==>C  to  ( [(a1,b1),...,(an,bn)] , C )     
   5.116 +    (a1=?=b1)==>...(an=?=bn)==>C  to  ( [(a1,b1),...,(an,bn)] , C )	
   5.117    [Tail recursive in order to return a pair of results] *)
   5.118  fun strip_flex_aux (pairs, Const("==>", _) $ (Const("=?=",_)$t$u) $ C) =
   5.119          strip_flex_aux ((t,u)::pairs, C)
   5.120 @@ -130,7 +130,7 @@
   5.121  
   5.122  (*Discard flexflex pairs*)
   5.123  fun skip_flexpairs (Const("==>", _) $ (Const("=?=",_)$_$_) $ C) =
   5.124 -        skip_flexpairs C
   5.125 +	skip_flexpairs C
   5.126    | skip_flexpairs C = C;
   5.127  
   5.128  (*strip a proof state (Horn clause): 
   5.129 @@ -165,13 +165,13 @@
   5.130  fun t occs u = (t aconv u) orelse 
   5.131        (case u of
   5.132            Abs(_,_,body) => t occs body
   5.133 -        | f$t' => t occs f  orelse  t occs t'
   5.134 -        | _ => false);
   5.135 +	| f$t' => t occs f  orelse  t occs t'
   5.136 +	| _ => false);
   5.137  
   5.138  (*Close up a formula over all free variables by quantification*)
   5.139  fun close_form A =
   5.140      list_all_free (map dest_Free (sort atless (term_frees A)),   
   5.141 -                   A);
   5.142 +		   A);
   5.143  
   5.144  
   5.145  (*Freeze all (T)Vars by turning them into (T)Frees*)
   5.146 @@ -188,9 +188,9 @@
   5.147    | thaw_vars(Free(a,T))  =
   5.148        let val T' = Type.thaw_vars T
   5.149        in case explode a of
   5.150 -           "?"::vn => let val (ixn,_) = Syntax.scan_varname vn
   5.151 +	   "?"::vn => let val (ixn,_) = Syntax.scan_varname vn
   5.152                        in Var(ixn,T') end
   5.153 -         | _       => Free(a,T')
   5.154 +	 | _       => Free(a,T')
   5.155        end
   5.156    | thaw_vars(Abs(a,T,t)) = Abs(a,Type.thaw_vars T, thaw_vars t)
   5.157    | thaw_vars(s$t)        = thaw_vars s $ thaw_vars t
   5.158 @@ -203,14 +203,14 @@
   5.159      result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   5.160  fun incr_indexes (Us: typ list, inc:int) t = 
   5.161    let fun incr (Var ((a,i), T), lev) = 
   5.162 -                Unify.combound (Var((a, i+inc), Us---> incr_tvar inc T),
   5.163 -                                lev, length Us)
   5.164 -        | incr (Abs (a,T,body), lev) =
   5.165 -                Abs (a, incr_tvar inc T, incr(body,lev+1))
   5.166 -        | incr (Const(a,T),_) = Const(a, incr_tvar inc T)
   5.167 -        | incr (Free(a,T),_) = Free(a, incr_tvar inc T)
   5.168 -        | incr (f$t, lev) = incr(f,lev) $ incr(t,lev)
   5.169 -        | incr (t,lev) = t
   5.170 +		Unify.combound (Var((a, i+inc), Us---> incr_tvar inc T),
   5.171 +				lev, length Us)
   5.172 +	| incr (Abs (a,T,body), lev) =
   5.173 +		Abs (a, incr_tvar inc T, incr(body,lev+1))
   5.174 +	| incr (Const(a,T),_) = Const(a, incr_tvar inc T)
   5.175 +	| incr (Free(a,T),_) = Free(a, incr_tvar inc T)
   5.176 +	| incr (f$t, lev) = incr(f,lev) $ incr(t,lev)
   5.177 +	| incr (t,lev) = t
   5.178    in  incr(t,0)  end;
   5.179  
   5.180  (*Make lifting functions from subgoal and increment.
   5.181 @@ -218,14 +218,14 @@
   5.182      lift_all operates on propositions     *)
   5.183  fun lift_fns (B,inc) =
   5.184    let fun lift_abs (Us, Const("==>", _) $ _ $ B) u = lift_abs (Us,B) u
   5.185 -        | lift_abs (Us, Const("all",_)$Abs(a,T,t)) u =
   5.186 -              Abs(a, T, lift_abs (T::Us, t) u)
   5.187 -        | lift_abs (Us, _) u = incr_indexes(rev Us, inc) u
   5.188 +	| lift_abs (Us, Const("all",_)$Abs(a,T,t)) u =
   5.189 +	      Abs(a, T, lift_abs (T::Us, t) u)
   5.190 +	| lift_abs (Us, _) u = incr_indexes(rev Us, inc) u
   5.191        fun lift_all (Us, Const("==>", _) $ A $ B) u =
   5.192 -              implies $ A $ lift_all (Us,B) u
   5.193 -        | lift_all (Us, Const("all",_)$Abs(a,T,t)) u = 
   5.194 -              all T $ Abs(a, T, lift_all (T::Us,t) u)
   5.195 -        | lift_all (Us, _) u = incr_indexes(rev Us, inc) u;
   5.196 +	      implies $ A $ lift_all (Us,B) u
   5.197 +	| lift_all (Us, Const("all",_)$Abs(a,T,t)) u = 
   5.198 +	      all T $ Abs(a, T, lift_all (T::Us,t) u)
   5.199 +	| lift_all (Us, _) u = incr_indexes(rev Us, inc) u;
   5.200    in  (lift_abs([],B), lift_all([],B))  end;
   5.201  
   5.202  (*Strips assumptions in goal, yielding list of hypotheses.   *)
   5.203 @@ -250,8 +250,8 @@
   5.204      if j=0 andalso n<=0 then A  (*nothing left to do...*)
   5.205      else case A of
   5.206          Const("==>", _) $ H $ B => 
   5.207 -          if n=1 then                           (remove_params j (n-1) B)
   5.208 -          else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   5.209 +	  if n=1 then                           (remove_params j (n-1) B)
   5.210 +	  else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   5.211        | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   5.212        | _ => if n>0 then raise TERM("remove_params", [A])
   5.213               else A;
   5.214 @@ -278,9 +278,9 @@
   5.215    if n>0 then deletes assumption n. *)
   5.216  fun flatten_params n A =
   5.217      let val params = strip_params A;
   5.218 -        val vars = if !auto_rename 
   5.219 -                   then rename_vars (!rename_prefix, params)
   5.220 -                   else variantlist(map #1 params,[]) ~~ map #2 params
   5.221 +	val vars = if !auto_rename 
   5.222 +		   then rename_vars (!rename_prefix, params)
   5.223 +		   else variantlist(map #1 params,[]) ~~ map #2 params
   5.224      in  list_all (vars, remove_params (length vars) n A)
   5.225      end;
   5.226  
   5.227 @@ -294,9 +294,9 @@
   5.228  (*Strips assumptions in goal yielding  ( [Hn,...,H1], [xm,...,x1], B )
   5.229    where H1,...,Hn are the hypotheses and x1...xm are the parameters.   *)
   5.230  fun strip_assums_aux (Hs, params, Const("==>", _) $ H $ B) = 
   5.231 -        strip_assums_aux (H::Hs, params, B)
   5.232 +	strip_assums_aux (H::Hs, params, B)
   5.233    | strip_assums_aux (Hs, params, Const("all",_)$Abs(a,T,t)) =
   5.234 -        strip_assums_aux (Hs, (a,T)::params, t)
   5.235 +	strip_assums_aux (Hs, (a,T)::params, t)
   5.236    | strip_assums_aux (Hs, params, B) = (Hs, params, B);
   5.237  
   5.238  fun strip_assums A = strip_assums_aux ([],[],A);
   5.239 @@ -310,7 +310,7 @@
   5.240        val D = Unify.rlist_abs(params, B)
   5.241        fun pairrev ([],pairs) = pairs  
   5.242          | pairrev (H::Hs,pairs) = 
   5.243 -            pairrev(Hs, (Unify.rlist_abs(params,H), D) :: pairs)
   5.244 +	    pairrev(Hs, (Unify.rlist_abs(params,H), D) :: pairs)
   5.245    in  pairrev (Hs,[])   (*WAS:  map pair (rev Hs)  *)
   5.246    end;
   5.247  
     6.1 --- a/src/Pure/net.ML	Mon Jan 29 13:58:15 1996 +0100
     6.2 +++ b/src/Pure/net.ML	Mon Jan 29 14:16:13 1996 +0100
     6.3 @@ -1,6 +1,6 @@
     6.4 -(*  Title:      net
     6.5 +(*  Title: 	net
     6.6      ID:         $Id$
     6.7 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.8 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     6.9      Copyright   1993  University of Cambridge
    6.10  
    6.11  Discrimination nets: a data structure for indexing items
    6.12 @@ -46,9 +46,9 @@
    6.13  *)
    6.14  fun add_key_of_terms (t, cs) = 
    6.15    let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs))
    6.16 -        | rands (Const(c,_), cs) = AtomK c :: cs
    6.17 -        | rands (Free(c,_),  cs) = AtomK c :: cs
    6.18 -        | rands (Bound i,  cs)   = AtomK (string_of_bound i) :: cs
    6.19 +	| rands (Const(c,_), cs) = AtomK c :: cs
    6.20 +	| rands (Free(c,_),  cs) = AtomK c :: cs
    6.21 +	| rands (Bound i,  cs)   = AtomK (string_of_bound i) :: cs
    6.22    in case (head_of t) of
    6.23        Var _ => VarK :: cs
    6.24      | Abs _ => VarK :: cs
    6.25 @@ -66,9 +66,9 @@
    6.26    Lookup functions preserve order in items stored at same level.
    6.27  *)
    6.28  datatype 'a net = Leaf of 'a list
    6.29 -                | Net of {comb: 'a net, 
    6.30 -                          var: 'a net,
    6.31 -                          alist: (string * 'a net) list};
    6.32 +		| Net of {comb: 'a net, 
    6.33 +			  var: 'a net,
    6.34 +			  alist: (string * 'a net) list};
    6.35  
    6.36  val empty = Leaf[];
    6.37  val emptynet = Net{comb=empty, var=empty, alist=[]};
    6.38 @@ -76,7 +76,7 @@
    6.39  
    6.40  (*** Insertion into a discrimination net ***)
    6.41  
    6.42 -exception INSERT;       (*duplicate item in the net*)
    6.43 +exception INSERT;	(*duplicate item in the net*)
    6.44  
    6.45  
    6.46  (*Adds item x to the list at the node addressed by the keys.
    6.47 @@ -89,25 +89,25 @@
    6.48              if gen_mem eq (x,xs) then  raise INSERT  else Leaf(x::xs)
    6.49          | ins1 (keys, Leaf[]) = ins1 (keys, emptynet)   (*expand empty...*)
    6.50          | ins1 (CombK :: keys, Net{comb,var,alist}) =
    6.51 -            Net{comb=ins1(keys,comb), var=var, alist=alist}
    6.52 -        | ins1 (VarK :: keys, Net{comb,var,alist}) =
    6.53 -            Net{comb=comb, var=ins1(keys,var), alist=alist}
    6.54 -        | ins1 (AtomK a :: keys, Net{comb,var,alist}) =
    6.55 -            let fun newpair net = (a, ins1(keys,net)) 
    6.56 -                fun inslist [] = [newpair empty]
    6.57 -                  | inslist((b: string, netb) :: alist) =
    6.58 -                      if a=b then newpair netb :: alist
    6.59 -                      else if a<b then (*absent, ins1ert in alist*)
    6.60 -                          newpair empty :: (b,netb) :: alist
    6.61 -                      else (*a>b*) (b,netb) :: inslist alist
    6.62 -            in  Net{comb=comb, var=var, alist= inslist alist}  end
    6.63 +	    Net{comb=ins1(keys,comb), var=var, alist=alist}
    6.64 +	| ins1 (VarK :: keys, Net{comb,var,alist}) =
    6.65 +	    Net{comb=comb, var=ins1(keys,var), alist=alist}
    6.66 +	| ins1 (AtomK a :: keys, Net{comb,var,alist}) =
    6.67 +	    let fun newpair net = (a, ins1(keys,net)) 
    6.68 +		fun inslist [] = [newpair empty]
    6.69 +		  | inslist((b: string, netb) :: alist) =
    6.70 +		      if a=b then newpair netb :: alist
    6.71 +		      else if a<b then (*absent, ins1ert in alist*)
    6.72 +			  newpair empty :: (b,netb) :: alist
    6.73 +		      else (*a>b*) (b,netb) :: inslist alist
    6.74 +	    in  Net{comb=comb, var=var, alist= inslist alist}  end
    6.75    in  ins1 (keys,net)  end;
    6.76  
    6.77  fun insert_term ((t,x), net, eq) = insert((key_of_term t, x), net, eq);
    6.78  
    6.79  (*** Deletion from a discrimination net ***)
    6.80  
    6.81 -exception DELETE;       (*missing item in the net*)
    6.82 +exception DELETE;	(*missing item in the net*)
    6.83  
    6.84  (*Create a new Net node if it would be nonempty*)
    6.85  fun newnet {comb=Leaf[], var=Leaf[], alist=[]} = empty
    6.86 @@ -124,19 +124,19 @@
    6.87    let fun del1 ([], Leaf xs) =
    6.88              if gen_mem eq (x,xs) then Leaf (gen_rem eq (xs,x))
    6.89              else raise DELETE
    6.90 -        | del1 (keys, Leaf[]) = raise DELETE
    6.91 -        | del1 (CombK :: keys, Net{comb,var,alist}) =
    6.92 -            newnet{comb=del1(keys,comb), var=var, alist=alist}
    6.93 -        | del1 (VarK :: keys, Net{comb,var,alist}) =
    6.94 -            newnet{comb=comb, var=del1(keys,var), alist=alist}
    6.95 -        | del1 (AtomK a :: keys, Net{comb,var,alist}) =
    6.96 -            let fun newpair net = (a, del1(keys,net)) 
    6.97 -                fun dellist [] = raise DELETE
    6.98 -                  | dellist((b: string, netb) :: alist) =
    6.99 -                      if a=b then conspair(newpair netb, alist)
   6.100 -                      else if a<b then (*absent*) raise DELETE
   6.101 -                      else (*a>b*)  (b,netb) :: dellist alist
   6.102 -            in  newnet{comb=comb, var=var, alist= dellist alist}  end
   6.103 +	| del1 (keys, Leaf[]) = raise DELETE
   6.104 +	| del1 (CombK :: keys, Net{comb,var,alist}) =
   6.105 +	    newnet{comb=del1(keys,comb), var=var, alist=alist}
   6.106 +	| del1 (VarK :: keys, Net{comb,var,alist}) =
   6.107 +	    newnet{comb=comb, var=del1(keys,var), alist=alist}
   6.108 +	| del1 (AtomK a :: keys, Net{comb,var,alist}) =
   6.109 +	    let fun newpair net = (a, del1(keys,net)) 
   6.110 +		fun dellist [] = raise DELETE
   6.111 +		  | dellist((b: string, netb) :: alist) =
   6.112 +		      if a=b then conspair(newpair netb, alist)
   6.113 +		      else if a<b then (*absent*) raise DELETE
   6.114 +		      else (*a>b*)  (b,netb) :: dellist alist
   6.115 +	    in  newnet{comb=comb, var=var, alist= dellist alist}  end
   6.116    in  del1 (keys,net)  end;
   6.117  
   6.118  fun delete_term ((t,x), net, eq) = delete((key_of_term t, x), net, eq);
   6.119 @@ -154,7 +154,7 @@
   6.120  
   6.121  (*Return the list of items at the given node, [] if no such node*)
   6.122  fun lookup (Leaf(xs), []) = xs
   6.123 -  | lookup (Leaf _, _::_) = []  (*non-empty keys and empty net*)
   6.124 +  | lookup (Leaf _, _::_) = []	(*non-empty keys and empty net*)
   6.125    | lookup (Net{comb,var,alist}, CombK :: keys) = lookup(comb,keys)
   6.126    | lookup (Net{comb,var,alist}, VarK :: keys) = lookup(var,keys)
   6.127    | lookup (Net{comb,var,alist}, AtomK a :: keys) = 
   6.128 @@ -166,7 +166,7 @@
   6.129    | net_skip (Net{comb,var,alist}, nets) = 
   6.130      foldr net_skip 
   6.131            (net_skip (comb,[]), 
   6.132 -           foldr (fn ((_,net), nets) => net::nets) (alist, var::nets));
   6.133 +	   foldr (fn ((_,net), nets) => net::nets) (alist, var::nets));
   6.134  
   6.135  (** Matching and Unification**)
   6.136  
   6.137 @@ -182,25 +182,25 @@
   6.138  *)
   6.139  fun matching unif t (net,nets) =
   6.140    let fun rands _ (Leaf _, nets) = nets
   6.141 -        | rands t (Net{comb,alist,...}, nets) =
   6.142 -            case t of 
   6.143 -                f$t => foldr (matching unif t) (rands f (comb,[]), nets)
   6.144 -              | Const(c,_) => look1 (alist, c) nets
   6.145 -              | Free(c,_)  => look1 (alist, c) nets
   6.146 -              | Bound i    => look1 (alist, string_of_bound i) nets
   6.147 -              | _          => nets
   6.148 +	| rands t (Net{comb,alist,...}, nets) =
   6.149 +	    case t of 
   6.150 +		f$t => foldr (matching unif t) (rands f (comb,[]), nets)
   6.151 +	      | Const(c,_) => look1 (alist, c) nets
   6.152 +	      | Free(c,_)  => look1 (alist, c) nets
   6.153 +	      | Bound i    => look1 (alist, string_of_bound i) nets
   6.154 +	      | _      	   => nets
   6.155    in 
   6.156       case net of
   6.157 -         Leaf _ => nets
   6.158 +	 Leaf _ => nets
   6.159         | Net{var,...} =>
   6.160 -           case (head_of t) of
   6.161 -               Var _ => if unif then net_skip (net,nets)
   6.162 -                        else var::nets          (*only matches Var in net*)
   6.163 +	   case (head_of t) of
   6.164 +	       Var _ => if unif then net_skip (net,nets)
   6.165 +			else var::nets	   	(*only matches Var in net*)
   6.166  (*If "unif" then a var instantiation in the abstraction could allow
   6.167    an eta-reduction, so regard the abstraction as a wildcard.*)
   6.168 -             | Abs _ => if unif then net_skip (net,nets)
   6.169 -                        else var::nets          (*only a Var can match*)
   6.170 -             | _ => rands t (net, var::nets)    (*var could match also*)
   6.171 +	     | Abs _ => if unif then net_skip (net,nets)
   6.172 +			else var::nets		(*only a Var can match*)
   6.173 +	     | _ => rands t (net, var::nets)	(*var could match also*)
   6.174    end;
   6.175  
   6.176  val extract_leaves = flat o map (fn Leaf(xs) => xs);
     7.1 --- a/src/Pure/pattern.ML	Mon Jan 29 13:58:15 1996 +0100
     7.2 +++ b/src/Pure/pattern.ML	Mon Jan 29 14:16:13 1996 +0100
     7.3 @@ -1,6 +1,6 @@
     7.4 -(*  Title:      pattern
     7.5 +(*  Title: 	pattern
     7.6      ID:         $Id$
     7.7 -    Author:     Tobias Nipkow and Christine Heinzelmann, TU Muenchen
     7.8 +    Author: 	Tobias Nipkow and Christine Heinzelmann, TU Muenchen
     7.9      Copyright   1993  TU Muenchen
    7.10  
    7.11  Unification of Higher-Order Patterns.
    7.12 @@ -229,8 +229,8 @@
    7.13  fun eta_contract (Abs(a,T,body)) = 
    7.14        (case eta_contract body  of
    7.15          body' as (f $ Bound i) => 
    7.16 -          if i=0 andalso not (0 mem loose_bnos f) then incr_boundvars ~1 f 
    7.17 -          else Abs(a,T,body')
    7.18 +	  if i=0 andalso not (0 mem loose_bnos f) then incr_boundvars ~1 f 
    7.19 +	  else Abs(a,T,body')
    7.20        | body' => Abs(a,T,body'))
    7.21    | eta_contract(f$t) = eta_contract f $ eta_contract t
    7.22    | eta_contract t = t;
    7.23 @@ -247,22 +247,22 @@
    7.24    Does not notice eta-equality, thus f does not match %(x)f(x)  *)
    7.25  fun fomatch tsig (pat,obj) =
    7.26    let fun typ_match args = (Type.typ_match tsig args)
    7.27 -                           handle Type.TYPE_MATCH => raise MATCH;
    7.28 +			   handle Type.TYPE_MATCH => raise MATCH;
    7.29        fun mtch (tyinsts,insts) = fn
    7.30 -        (Var(ixn,T), t)  =>
    7.31 -          if loose_bvar(t,0) then raise MATCH
    7.32 -          else (case assoc(insts,ixn) of
    7.33 -                  None => (typ_match (tyinsts, (T, fastype_of t)), 
    7.34 -                           (ixn,t)::insts)
    7.35 -                | Some u => if t aconv u then (tyinsts,insts) else raise MATCH)
    7.36 +	(Var(ixn,T), t)  =>
    7.37 +	  if loose_bvar(t,0) then raise MATCH
    7.38 +	  else (case assoc(insts,ixn) of
    7.39 +		  None => (typ_match (tyinsts, (T, fastype_of t)), 
    7.40 +			   (ixn,t)::insts)
    7.41 +		| Some u => if t aconv u then (tyinsts,insts) else raise MATCH)
    7.42        | (Free (a,T), Free (b,U)) =>
    7.43 -          if  a=b  then (typ_match (tyinsts,(T,U)), insts)  else raise MATCH
    7.44 +	  if  a=b  then (typ_match (tyinsts,(T,U)), insts)  else raise MATCH
    7.45        | (Const (a,T), Const (b,U))  =>
    7.46 -          if  a=b  then (typ_match (tyinsts,(T,U)), insts)  else raise MATCH
    7.47 +	  if  a=b  then (typ_match (tyinsts,(T,U)), insts)  else raise MATCH
    7.48        | (Bound i, Bound j)  =>
    7.49            if  i=j  then  (tyinsts,insts)  else raise MATCH
    7.50        | (Abs(_,T,t), Abs(_,U,u))  =>
    7.51 -          mtch (typ_match (tyinsts,(T,U)),insts) (t,u)
    7.52 +	  mtch (typ_match (tyinsts,(T,U)),insts) (t,u)
    7.53        | (f$t, g$u) => mtch (mtch (tyinsts,insts) (f,g)) (t, u)
    7.54        | _ => raise MATCH
    7.55    in mtch([],[]) (eta_contract pat,eta_contract obj) end;
     8.1 --- a/src/Pure/section_utils.ML	Mon Jan 29 13:58:15 1996 +0100
     8.2 +++ b/src/Pure/section_utils.ML	Mon Jan 29 14:16:13 1996 +0100
     8.3 @@ -1,6 +1,6 @@
     8.4 -(*  Title:      Pure/section-utils
     8.5 +(*  Title: 	Pure/section-utils
     8.6      ID:         $Id$
     8.7 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.8 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     8.9      Copyright   1994  University of Cambridge
    8.10  
    8.11  Utilities for writing new theory sections
    8.12 @@ -49,16 +49,16 @@
    8.13    Does not handle the \ddd form;  no error checking*)
    8.14  fun escape [] = []
    8.15    | escape cs = (case take_prefix (not o is_backslash) cs of
    8.16 -         (front, []) => front
    8.17 +	 (front, []) => front
    8.18         | (front, _::"n"::rest) => front @ ("\n" :: escape rest)
    8.19         | (front, _::"t"::rest) => front @ ("\t" :: escape rest)
    8.20         | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
    8.21         | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
    8.22         | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
    8.23         | (front, b::c::rest) => 
    8.24 -           if is_blank c   (*remove any further blanks and the following \ *)
    8.25 -           then front @ escape (tl (snd (take_prefix is_blank rest)))
    8.26 -           else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
    8.27 +	   if is_blank c   (*remove any further blanks and the following \ *)
    8.28 +	   then front @ escape (tl (snd (take_prefix is_blank rest)))
    8.29 +	   else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
    8.30  
    8.31  (*Remove the first and last charaters -- presumed to be quotes*)
    8.32  val trim = implode o escape o rev o tl o rev o tl o explode;
     9.1 --- a/src/Pure/sequence.ML	Mon Jan 29 13:58:15 1996 +0100
     9.2 +++ b/src/Pure/sequence.ML	Mon Jan 29 14:16:13 1996 +0100
     9.3 @@ -1,6 +1,6 @@
     9.4 -(*  Title:      sequence
     9.5 +(*  Title: 	sequence
     9.6      ID:         $Id$
     9.7 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.8 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     9.9      Copyright   1988  University of Cambridge
    9.10  
    9.11  Unbounded sequences implemented by closures.
    9.12 @@ -14,24 +14,24 @@
    9.13  signature SEQUENCE = 
    9.14    sig
    9.15    type 'a seq
    9.16 -  val append    : 'a seq * 'a seq -> 'a seq
    9.17 -  val chop      : int * 'a seq -> 'a list * 'a seq
    9.18 -  val cons      : 'a * 'a seq -> 'a seq
    9.19 -  val filters   : ('a -> bool) -> 'a seq -> 'a seq
    9.20 -  val flats     : 'a seq seq -> 'a seq
    9.21 -  val hd        : 'a seq -> 'a
    9.22 +  val append	: 'a seq * 'a seq -> 'a seq
    9.23 +  val chop	: int * 'a seq -> 'a list * 'a seq
    9.24 +  val cons	: 'a * 'a seq -> 'a seq
    9.25 +  val filters	: ('a -> bool) -> 'a seq -> 'a seq
    9.26 +  val flats	: 'a seq seq -> 'a seq
    9.27 +  val hd	: 'a seq -> 'a
    9.28    val interleave: 'a seq * 'a seq -> 'a seq
    9.29 -  val its_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
    9.30 -  val list_of_s : 'a seq -> 'a list
    9.31 -  val mapp      : ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
    9.32 -  val maps      : ('a -> 'b) -> 'a seq -> 'b seq
    9.33 -  val null      : 'a seq
    9.34 -  val prints    : (int -> 'a -> unit) -> int -> 'a seq -> unit
    9.35 -  val pull      : 'a seq -> ('a * 'a seq) option
    9.36 -  val s_of_list : 'a list -> 'a seq
    9.37 -  val seqof     : (unit -> ('a * 'a seq) option) -> 'a seq
    9.38 -  val single    : 'a -> 'a seq
    9.39 -  val tl        : 'a seq -> 'a seq
    9.40 +  val its_right	: ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
    9.41 +  val list_of_s	: 'a seq -> 'a list
    9.42 +  val mapp	: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
    9.43 +  val maps	: ('a -> 'b) -> 'a seq -> 'b seq
    9.44 +  val null	: 'a seq
    9.45 +  val prints	: (int -> 'a -> unit) -> int -> 'a seq -> unit
    9.46 +  val pull	: 'a seq -> ('a * 'a seq) option
    9.47 +  val s_of_list	: 'a list -> 'a seq
    9.48 +  val seqof	: (unit -> ('a * 'a seq) option) -> 'a seq
    9.49 +  val single	: 'a -> 'a seq
    9.50 +  val tl	: 'a seq -> 'a seq
    9.51    end;
    9.52  
    9.53  
    9.54 @@ -67,7 +67,7 @@
    9.55    else case pull(s) of
    9.56             None => ([],s)
    9.57           | Some(x,s') => let val (xs,s'') = chop (n-1,s')
    9.58 -                         in  (x::xs, s'')  end;
    9.59 +		         in  (x::xs, s'')  end;
    9.60  
    9.61  (*conversion from sequence to list*)
    9.62  fun list_of_s (s: 'a seq) : 'a list = case pull(s) of
    9.63 @@ -84,10 +84,10 @@
    9.64    the function prelem should print the element number and also the element*)
    9.65  fun prints (prelem: int -> 'a -> unit) count (s: 'a seq) : unit =
    9.66    let fun pr (k,s) = 
    9.67 -           if k>count then ()
    9.68 -           else case pull(s) of
    9.69 -               None => ()
    9.70 -             | Some(x,s') => (prelem k x;  prs"\n";  pr (k+1, s'))
    9.71 +	   if k>count then ()
    9.72 +	   else case pull(s) of
    9.73 +	       None => ()
    9.74 +	     | Some(x,s') => (prelem k x;  prs"\n";  pr (k+1, s'))
    9.75    in  pr(1,s)  end;
    9.76  
    9.77  (*Map the function f over the sequence, making a new sequence*)
    9.78 @@ -98,22 +98,22 @@
    9.79  (*Sequence append:  put the elements of xq in front of those of yq*)
    9.80  fun append (xq,yq)  =
    9.81    let fun copy xq = seqof (fn()=>
    9.82 -            case pull xq of  
    9.83 -                 None       => pull yq
    9.84 -               | Some(x,xq') => Some (x, copy xq'))
    9.85 +	    case pull xq of  
    9.86 +		 None       => pull yq
    9.87 +	       | Some(x,xq') => Some (x, copy xq'))
    9.88    in  copy xq end;
    9.89  
    9.90  (*Interleave elements of xq with those of yq -- fairer than append*)
    9.91  fun interleave (xq,yq) = seqof (fn()=>
    9.92        case pull(xq) of  
    9.93            None       => pull yq
    9.94 -        | Some(x,xq') => Some (x, interleave(yq, xq')));
    9.95 +	| Some(x,xq') => Some (x, interleave(yq, xq')));
    9.96  
    9.97  (*map over a sequence xq, append the sequence yq*)
    9.98  fun mapp f xq yq =
    9.99    let fun copy s = seqof (fn()=> 
   9.100              case pull(s) of
   9.101 -                None       => pull(yq)
   9.102 +	        None       => pull(yq)
   9.103                | Some(x,xq') => Some(f x, copy xq'))
   9.104    in  copy xq end;
   9.105  
   9.106 @@ -126,16 +126,16 @@
   9.107  fun its_right (f: 'a * 'b seq -> 'b seq) (s: 'a seq, bstr: 'b seq) : 'b seq =
   9.108    let fun its s = seqof (fn()=>
   9.109              case pull(s) of
   9.110 -                None       => pull bstr
   9.111 -              | Some(a,s') => pull(f(a, its s')))
   9.112 +	        None       => pull bstr
   9.113 +	      | Some(a,s') => pull(f(a, its s')))
   9.114    in  its s end; 
   9.115  
   9.116  fun filters pred xq =
   9.117    let fun copy s = seqof (fn()=> 
   9.118              case pull(s) of
   9.119 -                None       => None
   9.120 +	        None       => None
   9.121                | Some(x,xq') => if pred x then Some(x, copy xq')
   9.122 -                               else pull (copy xq') )
   9.123 +			       else pull (copy xq') )
   9.124    in  copy xq end
   9.125  
   9.126  end;
    10.1 --- a/src/Pure/sign.ML	Mon Jan 29 13:58:15 1996 +0100
    10.2 +++ b/src/Pure/sign.ML	Mon Jan 29 14:16:13 1996 +0100
    10.3 @@ -266,13 +266,13 @@
    10.4  (*Package error messages from type checking*)
    10.5  fun exn_type_msg sg (msg, Ts, ts) =
    10.6      let val show_typ = string_of_typ sg
    10.7 -        val show_term = string_of_term sg
    10.8 -        fun term_err [] = ""
    10.9 -          | term_err [t] = "\nInvolving this term:\n" ^ show_term t
   10.10 -          | term_err ts =
   10.11 -            "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
   10.12 +	val show_term = string_of_term sg
   10.13 +	fun term_err [] = ""
   10.14 +	  | term_err [t] = "\nInvolving this term:\n" ^ show_term t
   10.15 +	  | term_err ts =
   10.16 +	    "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
   10.17      in  "\nType checking error: " ^ msg ^ "\n" ^
   10.18 -        cat_lines (map show_typ Ts) ^ term_err ts ^ "\n"
   10.19 +	cat_lines (map show_typ Ts) ^ term_err ts ^ "\n"
   10.20      end; 
   10.21  
   10.22  
   10.23 @@ -308,7 +308,7 @@
   10.24  
   10.25      fun process_term(res,(t,i)) =
   10.26         let val ([u],tye) = 
   10.27 -               Type.infer_types(tsig,ct,types,sorts,used,freeze,[T'],[t])
   10.28 +	       Type.infer_types(tsig,ct,types,sorts,used,freeze,[T'],[t])
   10.29         in case res of
   10.30              One(_,t0,_) => Ambigs([u,t0])
   10.31            | Errs _ => One(i,u,tye)
   10.32 @@ -406,9 +406,9 @@
   10.33  fun ext_cnsts rd_const syn_only (syn, tsig, ctab) raw_consts =
   10.34    let
   10.35      fun prep_const (c, ty, mx) = 
   10.36 -          (c, 
   10.37 -           compress_type (varifyT (cert_typ tsig (no_tvars ty))), 
   10.38 -           mx)
   10.39 +	  (c, 
   10.40 +	   compress_type (varifyT (cert_typ tsig (no_tvars ty))), 
   10.41 +	   mx)
   10.42        handle TYPE (msg, _, _) => (writeln msg; err_in_const (Syntax.const_name c mx));
   10.43  
   10.44      val consts = map (prep_const o rd_const syn tsig) raw_consts;
    11.1 --- a/src/Pure/tactic.ML	Mon Jan 29 13:58:15 1996 +0100
    11.2 +++ b/src/Pure/tactic.ML	Mon Jan 29 14:16:13 1996 +0100
    11.3 @@ -1,6 +1,6 @@
    11.4 -(*  Title:      tactic
    11.5 +(*  Title: 	tactic
    11.6      ID:         $Id$
    11.7 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.8 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    11.9      Copyright   1991  University of Cambridge
   11.10  
   11.11  Tactics 
   11.12 @@ -83,8 +83,8 @@
   11.13  
   11.14  
   11.15  functor TacticFun (structure Logic: LOGIC and Drule: DRULE and 
   11.16 -                   Tactical: TACTICAL and Net: NET
   11.17 -          sharing Drule.Thm = Tactical.Thm) : TACTIC = 
   11.18 +		   Tactical: TACTICAL and Net: NET
   11.19 +	  sharing Drule.Thm = Tactical.Thm) : TACTIC = 
   11.20  struct
   11.21  structure Tactical = Tactical;
   11.22  structure Thm = Tactical.Thm;
   11.23 @@ -97,9 +97,9 @@
   11.24  (*Discover what goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
   11.25  fun trace_goalno_tac tf i = Tactic (fn state => 
   11.26      case Sequence.pull(tapply(tf i, state)) of
   11.27 -        None    => Sequence.null
   11.28 +	None    => Sequence.null
   11.29        | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
   11.30 -                         Sequence.seqof(fn()=> seqcell)));
   11.31 +    			 Sequence.seqof(fn()=> seqcell)));
   11.32  
   11.33  fun string_of (a,0) = a
   11.34    | string_of (a,i) = a ^ "_" ^ string_of_int i;
   11.35 @@ -109,22 +109,22 @@
   11.36    let val fth = freezeT th
   11.37        val {prop,sign,...} = rep_thm fth
   11.38        fun mk_inst (Var(v,T)) = 
   11.39 -          (cterm_of sign (Var(v,T)),
   11.40 -           cterm_of sign (Free(string_of v, T)))
   11.41 +	  (cterm_of sign (Var(v,T)),
   11.42 +	   cterm_of sign (Free(string_of v, T)))
   11.43        val insts = map mk_inst (term_vars prop)
   11.44    in  instantiate ([],insts) fth  end;
   11.45  
   11.46  (*Makes a rule by applying a tactic to an existing rule*)
   11.47  fun rule_by_tactic (Tactic tf) rl =
   11.48      case Sequence.pull(tf (freeze (standard rl))) of
   11.49 -        None        => raise THM("rule_by_tactic", 0, [rl])
   11.50 +	None        => raise THM("rule_by_tactic", 0, [rl])
   11.51        | Some(rl',_) => standard rl';
   11.52   
   11.53  (*** Basic tactics ***)
   11.54  
   11.55  (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
   11.56  fun PRIMSEQ thmfun = Tactic (fn state => thmfun state
   11.57 -                                         handle THM _ => Sequence.null);
   11.58 +			                 handle THM _ => Sequence.null);
   11.59  
   11.60  (*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
   11.61  fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun);
   11.62 @@ -164,9 +164,9 @@
   11.63  fun dresolve_tac rls = eresolve_tac (map make_elim rls);
   11.64  
   11.65  (*Shorthand versions: for resolution with a single theorem*)
   11.66 -fun rtac rl = rtac rl ;
   11.67 -fun etac rl = etac rl ;
   11.68 -fun dtac rl = dtac rl ;
   11.69 +fun rtac rl = resolve_tac [rl];
   11.70 +fun etac rl = eresolve_tac [rl];
   11.71 +fun dtac rl = dresolve_tac [rl];
   11.72  val atac = assume_tac;
   11.73  
   11.74  (*Use an assumption or some rules ... A popular combination!*)
   11.75 @@ -185,19 +185,19 @@
   11.76  fun lift_inst_rule (state, i, sinsts, rule) =
   11.77  let val {maxidx,sign,...} = rep_thm state
   11.78      val (_, _, Bi, _) = dest_state(state,i)
   11.79 -    val params = Logic.strip_params Bi          (*params of subgoal i*)
   11.80 +    val params = Logic.strip_params Bi	        (*params of subgoal i*)
   11.81      val params = rev(rename_wrt_term Bi params) (*as they are printed*)
   11.82      val paramTs = map #2 params
   11.83      and inc = maxidx+1
   11.84      fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T)
   11.85        | liftvar t = raise TERM("Variable expected", [t]);
   11.86      fun liftterm t = list_abs_free (params, 
   11.87 -                                    Logic.incr_indexes(paramTs,inc) t)
   11.88 +				    Logic.incr_indexes(paramTs,inc) t)
   11.89      (*Lifts instantiation pair over params*)
   11.90      fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
   11.91      fun lifttvar((a,i),ctyp) =
   11.92 -        let val {T,sign} = rep_ctyp ctyp
   11.93 -        in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
   11.94 +	let val {T,sign} = rep_ctyp ctyp
   11.95 +	in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
   11.96      val rts = types_sorts rule and (types,sorts) = types_sorts state
   11.97      fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
   11.98        | types'(ixn) = types ixn;
   11.99 @@ -215,10 +215,10 @@
  11.100  (*compose version: arguments are as for bicompose.*)
  11.101  fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i =
  11.102    STATE ( fn state => 
  11.103 -           compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule),
  11.104 -                        nsubgoal) i
  11.105 -           handle TERM (msg,_) => (writeln msg;  no_tac)
  11.106 -                | THM  (msg,_,_) => (writeln msg;  no_tac) );
  11.107 +	   compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule),
  11.108 +			nsubgoal) i
  11.109 +	   handle TERM (msg,_) => (writeln msg;  no_tac)
  11.110 +		| THM  (msg,_,_) => (writeln msg;  no_tac) );
  11.111  
  11.112  (*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
  11.113    terms that are substituted contain (term or type) unknowns from the
  11.114 @@ -242,8 +242,8 @@
  11.115    let val {maxidx,...} = rep_thm rl
  11.116        fun cvar ixn = cterm_of Sign.proto_pure (Var(ixn,propT));
  11.117        val revcut_rl' = 
  11.118 -          instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
  11.119 -                             (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
  11.120 +	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
  11.121 +			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
  11.122        val arg = (false, rl, nprems_of rl)
  11.123        val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl')
  11.124    in  th  end
  11.125 @@ -262,7 +262,7 @@
  11.126  
  11.127  (*Used by metacut_tac*)
  11.128  fun bires_cut_tac arg i =
  11.129 -    rtac cut_rl i  THEN  biresolve_tac arg (i+1) ;
  11.130 +    resolve_tac [cut_rl] i  THEN  biresolve_tac arg (i+1) ;
  11.131  
  11.132  (*The conclusion of the rule gets assumed in subgoal i,
  11.133    while subgoal i+1,... are the premises of the rule.*)
  11.134 @@ -271,7 +271,7 @@
  11.135  (*Recognizes theorems that are not rules, but simple propositions*)
  11.136  fun is_fact rl =
  11.137      case prems_of rl of
  11.138 -        [] => true  |  _::_ => false;
  11.139 +	[] => true  |  _::_ => false;
  11.140  
  11.141  (*"Cut" all facts from theorem list into the goal as assumptions. *)
  11.142  fun cut_facts_tac ths i =
  11.143 @@ -287,15 +287,15 @@
  11.144  (**** Indexing and filtering of theorems ****)
  11.145  
  11.146  (*Returns the list of potentially resolvable theorems for the goal "prem",
  11.147 -        using the predicate  could(subgoal,concl).
  11.148 +	using the predicate  could(subgoal,concl).
  11.149    Resulting list is no longer than "limit"*)
  11.150  fun filter_thms could (limit, prem, ths) =
  11.151    let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
  11.152        fun filtr (limit, []) = []
  11.153 -        | filtr (limit, th::ths) =
  11.154 -            if limit=0 then  []
  11.155 -            else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
  11.156 -            else filtr(limit,ths)
  11.157 +	| filtr (limit, th::ths) =
  11.158 +	    if limit=0 then  []
  11.159 +	    else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
  11.160 +	    else filtr(limit,ths)
  11.161    in  filtr(limit,ths)  end;
  11.162  
  11.163  
  11.164 @@ -320,9 +320,9 @@
  11.165  (*insert one tagged brl into the pair of nets*)
  11.166  fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =
  11.167      if eres then 
  11.168 -        case prems_of th of
  11.169 -            prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
  11.170 -          | [] => error"insert_tagged_brl: elimination rule with no premises"
  11.171 +	case prems_of th of
  11.172 +	    prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
  11.173 +	  | [] => error"insert_tagged_brl: elimination rule with no premises"
  11.174      else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
  11.175  
  11.176  (*build a pair of nets for biresolution*)
  11.177 @@ -366,9 +366,9 @@
  11.178      (fn (prem,i) =>
  11.179        let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
  11.180        in 
  11.181 -         if pred krls  
  11.182 +	 if pred krls  
  11.183           then PRIMSEQ
  11.184 -                (biresolution match (map (pair false) (orderlist krls)) i)
  11.185 +		(biresolution match (map (pair false) (orderlist krls)) i)
  11.186           else no_tac
  11.187        end);
  11.188  
  11.189 @@ -414,7 +414,7 @@
  11.190  (*Rewrite subgoals only, not main goal. *)
  11.191  fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
  11.192  
  11.193 -fun rewtac def = rewtac def;
  11.194 +fun rewtac def = rewrite_goals_tac [def];
  11.195  
  11.196  
  11.197  (*** Tactic for folding definitions, handling critical pairs ***)
  11.198 @@ -451,7 +451,7 @@
  11.199    in  
  11.200    if !Logic.auto_rename 
  11.201    then (writeln"Note: setting Logic.auto_rename := false"; 
  11.202 -        Logic.auto_rename := false)
  11.203 +	Logic.auto_rename := false)
  11.204    else ();
  11.205    case #2 (take_prefix (is_letdig orf is_blank) cs) of
  11.206        [] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i))
    12.1 --- a/src/Pure/tctical.ML	Mon Jan 29 13:58:15 1996 +0100
    12.2 +++ b/src/Pure/tctical.ML	Mon Jan 29 14:16:13 1996 +0100
    12.3 @@ -1,6 +1,6 @@
    12.4 -(*  Title:      tctical
    12.5 +(*  Title: 	tctical
    12.6      ID:         $Id$
    12.7 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.8 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    12.9      Copyright   1993  University of Cambridge
   12.10  
   12.11  Tacticals
   12.12 @@ -17,65 +17,65 @@
   12.13    structure Thm : THM
   12.14    local open Thm  in
   12.15    datatype tactic = Tactic of thm -> thm Sequence.seq
   12.16 -  val all_tac           : tactic
   12.17 -  val ALLGOALS          : (int -> tactic) -> tactic   
   12.18 -  val APPEND            : tactic * tactic -> tactic
   12.19 -  val APPEND'           : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   12.20 -  val BEST_FIRST        : (thm -> bool) * (thm -> int) -> tactic -> tactic
   12.21 -  val BREADTH_FIRST     : (thm -> bool) -> tactic -> tactic
   12.22 -  val CHANGED           : tactic -> tactic
   12.23 -  val COND              : (thm -> bool) -> tactic -> tactic -> tactic   
   12.24 -  val DEPTH_FIRST       : (thm -> bool) -> tactic -> tactic
   12.25 -  val DEPTH_SOLVE       : tactic -> tactic
   12.26 -  val DEPTH_SOLVE_1     : tactic -> tactic
   12.27 -  val DETERM            : tactic -> tactic
   12.28 -  val EVERY             : tactic list -> tactic   
   12.29 -  val EVERY'            : ('a -> tactic) list -> 'a -> tactic
   12.30 -  val EVERY1            : (int -> tactic) list -> tactic
   12.31 -  val FILTER            : (thm -> bool) -> tactic -> tactic
   12.32 -  val FIRST             : tactic list -> tactic   
   12.33 -  val FIRST'            : ('a -> tactic) list -> 'a -> tactic
   12.34 -  val FIRST1            : (int -> tactic) list -> tactic
   12.35 -  val FIRSTGOAL         : (int -> tactic) -> tactic
   12.36 -  val goals_limit       : int ref
   12.37 -  val has_fewer_prems   : int -> thm -> bool   
   12.38 -  val IF_UNSOLVED       : tactic -> tactic
   12.39 -  val INTLEAVE          : tactic * tactic -> tactic
   12.40 -  val INTLEAVE'         : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   12.41 -  val METAHYPS          : (thm list -> tactic) -> int -> tactic
   12.42 -  val no_tac            : tactic
   12.43 -  val ORELSE            : tactic * tactic -> tactic
   12.44 -  val ORELSE'           : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   12.45 -  val pause_tac         : tactic
   12.46 -  val print_tac         : tactic
   12.47 -  val REPEAT            : tactic -> tactic
   12.48 -  val REPEAT1           : tactic -> tactic
   12.49 -  val REPEAT_DETERM_N   : int -> tactic -> tactic
   12.50 -  val REPEAT_DETERM     : tactic -> tactic
   12.51 -  val REPEAT_DETERM1    : tactic -> tactic
   12.52 +  val all_tac		: tactic
   12.53 +  val ALLGOALS		: (int -> tactic) -> tactic   
   12.54 +  val APPEND		: tactic * tactic -> tactic
   12.55 +  val APPEND'		: ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   12.56 +  val BEST_FIRST	: (thm -> bool) * (thm -> int) -> tactic -> tactic
   12.57 +  val BREADTH_FIRST	: (thm -> bool) -> tactic -> tactic
   12.58 +  val CHANGED		: tactic -> tactic
   12.59 +  val COND		: (thm -> bool) -> tactic -> tactic -> tactic   
   12.60 +  val DEPTH_FIRST	: (thm -> bool) -> tactic -> tactic
   12.61 +  val DEPTH_SOLVE	: tactic -> tactic
   12.62 +  val DEPTH_SOLVE_1	: tactic -> tactic
   12.63 +  val DETERM		: tactic -> tactic
   12.64 +  val EVERY		: tactic list -> tactic   
   12.65 +  val EVERY'		: ('a -> tactic) list -> 'a -> tactic
   12.66 +  val EVERY1		: (int -> tactic) list -> tactic
   12.67 +  val FILTER		: (thm -> bool) -> tactic -> tactic
   12.68 +  val FIRST		: tactic list -> tactic   
   12.69 +  val FIRST'		: ('a -> tactic) list -> 'a -> tactic
   12.70 +  val FIRST1		: (int -> tactic) list -> tactic
   12.71 +  val FIRSTGOAL		: (int -> tactic) -> tactic
   12.72 +  val goals_limit	: int ref
   12.73 +  val has_fewer_prems	: int -> thm -> bool   
   12.74 +  val IF_UNSOLVED	: tactic -> tactic
   12.75 +  val INTLEAVE		: tactic * tactic -> tactic
   12.76 +  val INTLEAVE'		: ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   12.77 +  val METAHYPS		: (thm list -> tactic) -> int -> tactic
   12.78 +  val no_tac		: tactic
   12.79 +  val ORELSE		: tactic * tactic -> tactic
   12.80 +  val ORELSE'		: ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   12.81 +  val pause_tac		: tactic
   12.82 +  val print_tac		: tactic
   12.83 +  val REPEAT		: tactic -> tactic
   12.84 +  val REPEAT1		: tactic -> tactic
   12.85 +  val REPEAT_DETERM_N	: int -> tactic -> tactic
   12.86 +  val REPEAT_DETERM	: tactic -> tactic
   12.87 +  val REPEAT_DETERM1	: tactic -> tactic
   12.88    val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic
   12.89    val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
   12.90 -  val REPEAT_FIRST      : (int -> tactic) -> tactic
   12.91 -  val REPEAT_SOME       : (int -> tactic) -> tactic
   12.92 -  val SELECT_GOAL       : tactic -> int -> tactic
   12.93 -  val SOMEGOAL          : (int -> tactic) -> tactic   
   12.94 -  val STATE             : (thm -> tactic) -> tactic
   12.95 -  val strip_context     : term -> (string * typ) list * term list * term
   12.96 -  val SUBGOAL           : ((term*int) -> tactic) -> int -> tactic
   12.97 -  val suppress_tracing  : bool ref
   12.98 -  val tapply            : tactic * thm -> thm Sequence.seq
   12.99 -  val THEN              : tactic * tactic -> tactic
  12.100 -  val THEN'             : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
  12.101 -  val THEN_BEST_FIRST   : tactic * ((thm->bool) * (thm->int) * tactic) 
  12.102 -                          -> tactic
  12.103 -  val THEN_ELSE         : tactic * (tactic*tactic) -> tactic
  12.104 -  val traced_tac        : (thm -> (thm * thm Sequence.seq) option) -> tactic
  12.105 -  val tracify           : bool ref -> tactic -> thm -> thm Sequence.seq
  12.106 -  val trace_BEST_FIRST  : bool ref
  12.107 -  val trace_DEPTH_FIRST : bool ref
  12.108 -  val trace_REPEAT      : bool ref
  12.109 -  val TRY               : tactic -> tactic
  12.110 -  val TRYALL            : (int -> tactic) -> tactic   
  12.111 +  val REPEAT_FIRST	: (int -> tactic) -> tactic
  12.112 +  val REPEAT_SOME	: (int -> tactic) -> tactic
  12.113 +  val SELECT_GOAL	: tactic -> int -> tactic
  12.114 +  val SOMEGOAL		: (int -> tactic) -> tactic   
  12.115 +  val STATE		: (thm -> tactic) -> tactic
  12.116 +  val strip_context	: term -> (string * typ) list * term list * term
  12.117 +  val SUBGOAL		: ((term*int) -> tactic) -> int -> tactic
  12.118 +  val suppress_tracing	: bool ref
  12.119 +  val tapply		: tactic * thm -> thm Sequence.seq
  12.120 +  val THEN		: tactic * tactic -> tactic
  12.121 +  val THEN'		: ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
  12.122 +  val THEN_BEST_FIRST	: tactic * ((thm->bool) * (thm->int) * tactic) 
  12.123 +			  -> tactic
  12.124 +  val THEN_ELSE		: tactic * (tactic*tactic) -> tactic
  12.125 +  val traced_tac	: (thm -> (thm * thm Sequence.seq) option) -> tactic
  12.126 +  val tracify		: bool ref -> tactic -> thm -> thm Sequence.seq
  12.127 +  val trace_BEST_FIRST	: bool ref
  12.128 +  val trace_DEPTH_FIRST	: bool ref
  12.129 +  val trace_REPEAT	: bool ref
  12.130 +  val TRY		: tactic -> tactic
  12.131 +  val TRYALL		: (int -> tactic) -> tactic   
  12.132    end
  12.133    end;
  12.134  
  12.135 @@ -115,7 +115,7 @@
  12.136  fun (Tactic tf1)  ORELSE  (Tactic tf2) = 
  12.137    Tactic (fn state =>  
  12.138      case Sequence.pull(tf1 state) of
  12.139 -        None       => tf2 state
  12.140 +	None       => tf2 state
  12.141        | sequencecell => Sequence.seqof(fn()=> sequencecell));
  12.142  
  12.143  
  12.144 @@ -132,15 +132,15 @@
  12.145                            Sequence.seqof(fn()=> Sequence.pull (tf2 state))));
  12.146  
  12.147  (*Conditional tactic.
  12.148 -        tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
  12.149 -        tac1 THEN tac2   = tac1 THEN_ELSE (tac2, no_tac)
  12.150 +	tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
  12.151 +	tac1 THEN tac2   = tac1 THEN_ELSE (tac2, no_tac)
  12.152  *)
  12.153  fun (Tactic tf) THEN_ELSE (Tactic tf1, Tactic tf2) = 
  12.154    Tactic (fn state =>  
  12.155      case Sequence.pull(tf state) of
  12.156 -        None    => tf2 state            (*failed; try tactic 2*)
  12.157 -      | seqcell => Sequence.flats       (*succeeded; use tactic 1*)
  12.158 -                    (Sequence.maps tf1 (Sequence.seqof(fn()=> seqcell))));
  12.159 +	None    => tf2 state		(*failed; try tactic 2*)
  12.160 +      | seqcell => Sequence.flats 	(*succeeded; use tactic 1*)
  12.161 +	            (Sequence.maps tf1 (Sequence.seqof(fn()=> seqcell))));
  12.162  
  12.163  
  12.164  (*Versions for combining tactic-valued functions, as in
  12.165 @@ -160,7 +160,7 @@
  12.166  (*Make a tactic deterministic by chopping the tail of the proof sequence*)
  12.167  fun DETERM (Tactic tf) = Tactic (fn state => 
  12.168        case Sequence.pull (tf state) of
  12.169 -              None => Sequence.null
  12.170 +	      None => Sequence.null
  12.171              | Some(x,_) => Sequence.cons(x, Sequence.null));
  12.172  
  12.173  
  12.174 @@ -242,15 +242,15 @@
  12.175  fun tracify flag (Tactic tf) state =
  12.176    if !flag andalso not (!suppress_tracing)
  12.177             then (!print_goals_ref (!goals_limit) state;  
  12.178 -                 prs"** Press RETURN to continue: ";
  12.179 -                 exec_trace_command flag (tf,state))
  12.180 +		 prs"** Press RETURN to continue: ";
  12.181 +		 exec_trace_command flag (tf,state))
  12.182    else tf state;
  12.183  
  12.184  (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)
  12.185  fun traced_tac seqf = Tactic (fn st =>
  12.186      (suppress_tracing := false;
  12.187       Sequence.seqof (fn()=> seqf st
  12.188 -                         handle TRACE_EXIT st' => Some(st', Sequence.null))));
  12.189 +		         handle TRACE_EXIT st' => Some(st', Sequence.null))));
  12.190  
  12.191  
  12.192  (*Deterministic REPEAT: only retains the first outcome; 
  12.193 @@ -259,10 +259,10 @@
  12.194  fun REPEAT_DETERM_N n tac = 
  12.195    let val tf = tracify trace_REPEAT tac
  12.196        fun drep 0 st = Some(st, Sequence.null)
  12.197 -        | drep n st =
  12.198 -           (case Sequence.pull(tf st) of
  12.199 -                None       => Some(st, Sequence.null)
  12.200 -              | Some(st',_) => drep (n-1) st')
  12.201 +	| drep n st =
  12.202 +	   (case Sequence.pull(tf st) of
  12.203 +		None       => Some(st, Sequence.null)
  12.204 +	      | Some(st',_) => drep (n-1) st')
  12.205    in  traced_tac (drep n)  end;
  12.206  
  12.207  (*Allows any number of repetitions*)
  12.208 @@ -272,12 +272,12 @@
  12.209  fun REPEAT tac = 
  12.210    let val tf = tracify trace_REPEAT tac
  12.211        fun rep qs st = 
  12.212 -        case Sequence.pull(tf st) of
  12.213 -            None       => Some(st, Sequence.seqof(fn()=> repq qs))
  12.214 +	case Sequence.pull(tf st) of
  12.215 +  	    None       => Some(st, Sequence.seqof(fn()=> repq qs))
  12.216            | Some(st',q) => rep (q::qs) st'
  12.217        and repq [] = None
  12.218          | repq(q::qs) = case Sequence.pull q of
  12.219 -            None       => repq qs
  12.220 +  	    None       => repq qs
  12.221            | Some(st,q) => rep (q::qs) st
  12.222    in  traced_tac (rep [])  end;
  12.223  
  12.224 @@ -294,13 +294,13 @@
  12.225   let val tf = tracify trace_DEPTH_FIRST tac
  12.226       fun depth used [] = None
  12.227         | depth used (q::qs) =
  12.228 -          case Sequence.pull q of
  12.229 -              None         => depth used qs
  12.230 -            | Some(st,stq) => 
  12.231 -                if satp st andalso not (gen_mem eq_thm (st, used))
  12.232 -                then Some(st, Sequence.seqof
  12.233 -                                 (fn()=> depth (st::used) (stq::qs)))
  12.234 -                else depth used (tf st :: stq :: qs)
  12.235 +	  case Sequence.pull q of
  12.236 +	      None         => depth used qs
  12.237 +	    | Some(st,stq) => 
  12.238 +		if satp st andalso not (gen_mem eq_thm (st, used))
  12.239 +		then Some(st, Sequence.seqof
  12.240 +			         (fn()=> depth (st::used) (stq::qs)))
  12.241 +		else depth used (tf st :: stq :: qs)
  12.242    in  traced_tac (fn st => depth [] ([Sequence.single st]))  end;
  12.243  
  12.244  
  12.245 @@ -316,7 +316,7 @@
  12.246  fun DEPTH_SOLVE_1 tac = STATE
  12.247   (fn state => 
  12.248      (case nprems_of state of
  12.249 -        0 => no_tac
  12.250 +	0 => no_tac
  12.251        | n => DEPTH_FIRST (has_fewer_prems n) tac));
  12.252  
  12.253  (*Uses depth-first search to solve ALL subgoals*)
  12.254 @@ -344,17 +344,17 @@
  12.255    let val tf = tracify trace_BEST_FIRST tac
  12.256        fun pairsize th = (sizef th, th);
  12.257        fun bfs (news,nprfs) =
  12.258 -           (case  partition satp news  of
  12.259 -                ([],nonsats) => next(foldr insert
  12.260 -                                        (map pairsize nonsats, nprfs)) 
  12.261 -              | (sats,_)  => some_of_list sats)
  12.262 +	   (case  partition satp news  of
  12.263 +		([],nonsats) => next(foldr insert
  12.264 +					(map pairsize nonsats, nprfs)) 
  12.265 +	      | (sats,_)  => some_of_list sats)
  12.266        and next [] = None
  12.267          | next ((n,prf)::nprfs) =
  12.268 -            (if !trace_BEST_FIRST 
  12.269 -               then writeln("state size = " ^ string_of_int n ^ 
  12.270 -                         "  queue length =" ^ string_of_int (length nprfs))  
  12.271 +	    (if !trace_BEST_FIRST 
  12.272 +	       then writeln("state size = " ^ string_of_int n ^ 
  12.273 +		         "  queue length =" ^ string_of_int (length nprfs))  
  12.274                 else ();
  12.275 -             bfs (Sequence.list_of_s (tf prf), nprfs))
  12.276 +	     bfs (Sequence.list_of_s (tf prf), nprfs))
  12.277        fun tf st = bfs (Sequence.list_of_s (tf0 st),  [])
  12.278    in traced_tac tf end;
  12.279  
  12.280 @@ -366,12 +366,12 @@
  12.281  fun BREADTH_FIRST satpred (Tactic tf) = 
  12.282    let val tacf = Sequence.list_of_s o tf;
  12.283        fun bfs prfs =
  12.284 -         (case  partition satpred prfs  of
  12.285 -              ([],[]) => []
  12.286 -            | ([],nonsats) => 
  12.287 -                  (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
  12.288 -                   bfs (flat (map tacf nonsats)))
  12.289 -            | (sats,_)  => sats)
  12.290 +	 (case  partition satpred prfs  of
  12.291 +	      ([],[]) => []
  12.292 +	    | ([],nonsats) => 
  12.293 +		  (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
  12.294 +		   bfs (flat (map tacf nonsats)))
  12.295 +	    | (sats,_)  => sats)
  12.296    in Tactic (fn state => Sequence.s_of_list (bfs [state])) end;
  12.297  
  12.298  
  12.299 @@ -395,13 +395,13 @@
  12.300    Essential to work backwards since tf(i) may add/delete subgoals at i. *)
  12.301  fun ALLGOALS tf = 
  12.302    let fun tac 0 = all_tac
  12.303 -        | tac n = tf(n) THEN tac(n-1)
  12.304 +	| tac n = tf(n) THEN tac(n-1)
  12.305    in  Tactic(fn state => tapply(tac(nprems_of state), state))  end;
  12.306  
  12.307  (*For n subgoals, performs tf(n) ORELSE ... ORELSE tf(1)  *)
  12.308  fun SOMEGOAL tf = 
  12.309    let fun tac 0 = no_tac
  12.310 -        | tac n = tf(n) ORELSE tac(n-1)
  12.311 +	| tac n = tf(n) ORELSE tac(n-1)
  12.312    in  Tactic(fn state => tapply(tac(nprems_of state), state))  end;
  12.313  
  12.314  (*For n subgoals, performs tf(1) ORELSE ... ORELSE tf(n).
  12.315 @@ -442,8 +442,8 @@
  12.316  (* Prevent the subgoal's assumptions from becoming additional subgoals in the
  12.317     new proof state by enclosing them by a universal quantification *)
  12.318  fun protect_subgoal state i =
  12.319 -        Sequence.hd (bicompose false (false,dummy_quant_rl,1) i state)
  12.320 -        handle _ => error"SELECT_GOAL -- impossible error???";
  12.321 +	Sequence.hd (bicompose false (false,dummy_quant_rl,1) i state)
  12.322 +	handle _ => error"SELECT_GOAL -- impossible error???";
  12.323  
  12.324  (*Does the work of SELECT_GOAL. *)
  12.325  fun select (Tactic tf) state i =
  12.326 @@ -465,10 +465,10 @@
  12.327    Main difference from strip_assums concerns parameters: 
  12.328      it replaces the bound variables by free variables.  *)
  12.329  fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) = 
  12.330 -        strip_context_aux (params, H::Hs, B)
  12.331 +	strip_context_aux (params, H::Hs, B)
  12.332    | strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) =
  12.333          let val (b,u) = variant_abs(a,T,t)
  12.334 -        in  strip_context_aux ((b,T)::params, Hs, u)  end
  12.335 +	in  strip_context_aux ((b,T)::params, Hs, u)  end
  12.336    | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
  12.337  
  12.338  fun strip_context A = strip_context_aux ([],[],A);
  12.339 @@ -498,7 +498,7 @@
  12.340  
  12.341    fun free_of s ((a,i), T) =
  12.342          Free(s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i),
  12.343 -             T)
  12.344 +	     T)
  12.345  
  12.346    fun mk_inst (var as Var(v,T))  = (var,  free_of "METAHYP1_" (v,T))
  12.347  in
  12.348 @@ -520,17 +520,17 @@
  12.349        (*Subgoal variables: make Free; lift type over params*)
  12.350        fun mk_subgoal_inst concl_vars (var as Var(v,T)) = 
  12.351            if var mem concl_vars 
  12.352 -          then (var, true, free_of "METAHYP2_" (v,T))
  12.353 -          else (var, false,
  12.354 -                free_of "METAHYP2_" (v, map #2 params --->T))
  12.355 +	  then (var, true, free_of "METAHYP2_" (v,T))
  12.356 +	  else (var, false,
  12.357 +		free_of "METAHYP2_" (v, map #2 params --->T))
  12.358        (*Instantiate subgoal vars by Free applied to params*)
  12.359        fun mk_ctpair (t,in_concl,u) = 
  12.360 -          if in_concl then (cterm t,  cterm u)
  12.361 +	  if in_concl then (cterm t,  cterm u)
  12.362            else (cterm t,  cterm (list_comb (u,fparams)))
  12.363        (*Restore Vars with higher type and index*)
  12.364        fun mk_subgoal_swap_ctpair 
  12.365 -                (t as Var((a,i),_), in_concl, u as Free(_,U)) = 
  12.366 -          if in_concl then (cterm u, cterm t)
  12.367 +		(t as Var((a,i),_), in_concl, u as Free(_,U)) = 
  12.368 +	  if in_concl then (cterm u, cterm t)
  12.369            else (cterm u, cterm(Var((a, i+maxidx), U)))
  12.370        (*Embed B in the original context of params and hyps*)
  12.371        fun embed B = list_all_free (params, list_implies (hyps, B))
  12.372 @@ -538,34 +538,34 @@
  12.373        fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
  12.374        (*Embed an ff pair in the original params*)
  12.375        fun embed_ff(t,u) = 
  12.376 -          mk_flexpair (list_abs_free (params, t), list_abs_free (params, u))
  12.377 +	  mk_flexpair (list_abs_free (params, t), list_abs_free (params, u))
  12.378        (*Remove parameter abstractions from the ff pairs*)
  12.379        fun elim_ff ff = flexpair_abs_elim_list cparams ff
  12.380        (*A form of lifting that discharges assumptions.*)
  12.381        fun relift st = 
  12.382 -        let val prop = #prop(rep_thm st)
  12.383 -            val subgoal_vars = (*Vars introduced in the subgoals*)
  12.384 -                  foldr add_term_vars (strip_imp_prems prop, [])
  12.385 -            and concl_vars = add_term_vars (strip_imp_concl prop, [])
  12.386 -            val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
  12.387 -            val st' = instantiate ([], map mk_ctpair subgoal_insts) st
  12.388 -            val emBs = map (cterm o embed) (prems_of st')
  12.389 +	let val prop = #prop(rep_thm st)
  12.390 +	    val subgoal_vars = (*Vars introduced in the subgoals*)
  12.391 +		  foldr add_term_vars (strip_imp_prems prop, [])
  12.392 +	    and concl_vars = add_term_vars (strip_imp_concl prop, [])
  12.393 +	    val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
  12.394 +	    val st' = instantiate ([], map mk_ctpair subgoal_insts) st
  12.395 +	    val emBs = map (cterm o embed) (prems_of st')
  12.396              and ffs = map (cterm o embed_ff) (tpairs_of st')
  12.397 -            val Cth  = implies_elim_list st' 
  12.398 -                            (map (elim_ff o assume) ffs @
  12.399 -                             map (elim o assume) emBs)
  12.400 -        in  (*restore the unknowns to the hypotheses*)
  12.401 -            free_instantiate (map swap_ctpair insts @
  12.402 -                              map mk_subgoal_swap_ctpair subgoal_insts)
  12.403 -                (*discharge assumptions from state in same order*)
  12.404 -                (implies_intr_list (ffs@emBs)
  12.405 -                  (forall_intr_list cparams (implies_intr_list chyps Cth)))
  12.406 -        end
  12.407 +	    val Cth  = implies_elim_list st' 
  12.408 +			    (map (elim_ff o assume) ffs @
  12.409 +			     map (elim o assume) emBs)
  12.410 +	in  (*restore the unknowns to the hypotheses*)
  12.411 +	    free_instantiate (map swap_ctpair insts @
  12.412 +			      map mk_subgoal_swap_ctpair subgoal_insts)
  12.413 +		(*discharge assumptions from state in same order*)
  12.414 +		(implies_intr_list (ffs@emBs)
  12.415 +		  (forall_intr_list cparams (implies_intr_list chyps Cth)))
  12.416 +	end
  12.417        val subprems = map (forall_elim_vars 0) hypths
  12.418        and st0 = trivial (cterm concl)
  12.419        (*function to replace the current subgoal*)
  12.420        fun next st = bicompose false (false, relift st, nprems_of st)
  12.421 -                    i state
  12.422 +	            i state
  12.423    in  Sequence.flats (Sequence.maps next (tapply(tacf subprems, st0)))
  12.424    end);
  12.425  end;
    13.1 --- a/src/Pure/term.ML	Mon Jan 29 13:58:15 1996 +0100
    13.2 +++ b/src/Pure/term.ML	Mon Jan 29 14:16:13 1996 +0100
    13.3 @@ -1,6 +1,6 @@
    13.4 -(*  Title:      Pure/term.ML
    13.5 +(*  Title: 	Pure/term.ML
    13.6      ID:         $Id$
    13.7 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.8 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    13.9      Copyright   Cambridge University 1992
   13.10  
   13.11  Simply typed lambda-calculus: types, terms, and basic operations
   13.12 @@ -26,7 +26,7 @@
   13.13  (* The sorts attached to TFrees and TVars specify the sort of that variable *)
   13.14  datatype typ = Type  of string * typ list
   13.15               | TFree of string * sort
   13.16 -             | TVar  of indexname * sort;
   13.17 +	     | TVar  of indexname * sort;
   13.18  
   13.19  fun S --> T = Type("fun",[S,T]);
   13.20  
   13.21 @@ -120,19 +120,19 @@
   13.22  fun type_of1 (Ts, Const (_,T)) = T
   13.23    | type_of1 (Ts, Free  (_,T)) = T
   13.24    | type_of1 (Ts, Bound i) = (nth_elem (i,Ts)  
   13.25 -        handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i]))
   13.26 +  	handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i]))
   13.27    | type_of1 (Ts, Var (_,T)) = T
   13.28    | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
   13.29    | type_of1 (Ts, f$u) = 
   13.30        let val U = type_of1(Ts,u)
   13.31            and T = type_of1(Ts,f)
   13.32        in case T of
   13.33 -            Type("fun",[T1,T2]) =>
   13.34 -              if T1=U then T2  else raise TYPE
   13.35 -                    ("type_of: type mismatch in application", [T1,U], [f$u])
   13.36 -          | _ => raise TYPE 
   13.37 -                    ("type_of: function type is expected in application",
   13.38 -                     [T,U], [f$u])
   13.39 +	    Type("fun",[T1,T2]) =>
   13.40 +	      if T1=U then T2  else raise TYPE
   13.41 +	            ("type_of: type mismatch in application", [T1,U], [f$u])
   13.42 +	  | _ => raise TYPE 
   13.43 +		    ("type_of: function type is expected in application",
   13.44 +		     [T,U], [f$u])
   13.45        end;
   13.46  
   13.47  fun type_of t : typ = type_of1 ([],t);
   13.48 @@ -140,12 +140,12 @@
   13.49  (*Determines the type of a term, with minimal checking*)
   13.50  fun fastype_of1 (Ts, f$u) = 
   13.51      (case fastype_of1 (Ts,f) of
   13.52 -        Type("fun",[_,T]) => T
   13.53 -        | _ => raise TERM("fastype_of: expected function type", [f$u]))
   13.54 +	Type("fun",[_,T]) => T
   13.55 +	| _ => raise TERM("fastype_of: expected function type", [f$u]))
   13.56    | fastype_of1 (_, Const (_,T)) = T
   13.57    | fastype_of1 (_, Free (_,T)) = T
   13.58    | fastype_of1 (Ts, Bound i) = (nth_elem(i,Ts)
   13.59 -         handle LIST _ => raise TERM("fastype_of: Bound", [Bound i]))
   13.60 +  	 handle LIST _ => raise TERM("fastype_of: Bound", [Bound i]))
   13.61    | fastype_of1 (_, Var (_,T)) = T 
   13.62    | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
   13.63  
   13.64 @@ -247,7 +247,7 @@
   13.65  
   13.66  (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
   13.67  fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
   13.68 -                (a,T) :: strip_all_vars t 
   13.69 +		(a,T) :: strip_all_vars t 
   13.70    | strip_all_vars t  =  [] : (string*typ) list;
   13.71  
   13.72  (*increments a term's non-local bound variables
   13.73 @@ -256,7 +256,7 @@
   13.74       lev is  level at which a bound variable is considered 'loose'*)
   13.75  fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u 
   13.76    | incr_bv (inc, lev, Abs(a,T,body)) =
   13.77 -        Abs(a, T, incr_bv(inc,lev+1,body))
   13.78 +	Abs(a, T, incr_bv(inc,lev+1,body))
   13.79    | incr_bv (inc, lev, f$t) = 
   13.80        incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   13.81    | incr_bv (inc, lev, u) = u;
   13.82 @@ -268,10 +268,10 @@
   13.83  (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   13.84     (Bound 0) is loose at level 0 *)
   13.85  fun add_loose_bnos (Bound i, lev, js) = 
   13.86 -        if i<lev then js  else  (i-lev) ins js
   13.87 +	if i<lev then js  else  (i-lev) ins js
   13.88    | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   13.89    | add_loose_bnos (f$t, lev, js) =
   13.90 -        add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
   13.91 +	add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
   13.92    | add_loose_bnos (_, _, js) = js;
   13.93  
   13.94  fun loose_bnos t = add_loose_bnos (t, 0, []);
   13.95 @@ -287,20 +287,20 @@
   13.96  (*Substitute arguments for loose bound variables.
   13.97    Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   13.98    Note that for ((x,y)c)(a,b), the bound vars in c are x=1 and y=0
   13.99 -        and the appropriate call is  subst_bounds([b,a], c) .
  13.100 +	and the appropriate call is  subst_bounds([b,a], c) .
  13.101    Loose bound variables >=n are reduced by "n" to
  13.102       compensate for the disappearance of lambdas.
  13.103  *)
  13.104  fun subst_bounds (args: term list, t) : term = 
  13.105    let val n = length args;
  13.106        fun subst (t as Bound i, lev) =
  13.107 -            if i<lev then  t    (*var is locally bound*)
  13.108 -            else  (case (drop (i-lev,args)) of
  13.109 -                  []     => Bound(i-n)  (*loose: change it*)
  13.110 -                | arg::_ => incr_boundvars lev arg)
  13.111 -        | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
  13.112 -        | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
  13.113 -        | subst (t,lev) = t
  13.114 + 	    if i<lev then  t    (*var is locally bound*)
  13.115 +	    else  (case (drop (i-lev,args)) of
  13.116 +		  []     => Bound(i-n)  (*loose: change it*)
  13.117 +	        | arg::_ => incr_boundvars lev arg)
  13.118 +	| subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
  13.119 +	| subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
  13.120 +	| subst (t,lev) = t
  13.121    in   case args of [] => t  | _ => subst (t,0)  end;
  13.122  
  13.123  (*beta-reduce if possible, else form application*)
  13.124 @@ -326,9 +326,9 @@
  13.125    Terms must be NORMAL.  Treats all Vars as distinct. *)
  13.126  fun could_unify (t,u) =
  13.127    let fun matchrands (f$t, g$u) = could_unify(t,u) andalso  matchrands(f,g)
  13.128 -        | matchrands _ = true
  13.129 +	| matchrands _ = true
  13.130    in case (head_of t , head_of u) of
  13.131 -        (_, Var _) => true
  13.132 +	(_, Var _) => true
  13.133        | (Var _, _) => true
  13.134        | (Const(a,_), Const(b,_)) =>  a=b andalso matchrands(t,u)
  13.135        | (Free(a,_), Free(b,_)) =>  a=b andalso matchrands(t,u)
  13.136 @@ -342,11 +342,11 @@
  13.137  fun subst_free [] = (fn t=>t)
  13.138    | subst_free pairs =
  13.139        let fun substf u = 
  13.140 -            case gen_assoc (op aconv) (pairs, u) of
  13.141 -                Some u' => u'
  13.142 -              | None => (case u of Abs(a,T,t) => Abs(a, T, substf t)
  13.143 -                                 | t$u' => substf t $ substf u'
  13.144 -                                 | _ => u)
  13.145 +	    case gen_assoc (op aconv) (pairs, u) of
  13.146 +		Some u' => u'
  13.147 +	      | None => (case u of Abs(a,T,t) => Abs(a, T, substf t)
  13.148 +				 | t$u' => substf t $ substf u'
  13.149 +				 | _ => u)
  13.150        in  substf  end;
  13.151  
  13.152  (*a total, irreflexive ordering on index names*)
  13.153 @@ -360,8 +360,8 @@
  13.154    let fun abst (lev,u) = if (v aconv u) then (Bound lev) else
  13.155        (case u of
  13.156            Abs(a,T,t) => Abs(a, T, abst(lev+1, t))
  13.157 -        | f$rand => abst(lev,f) $ abst(lev,rand)
  13.158 -        | _ => u)
  13.159 +	| f$rand => abst(lev,f) $ abst(lev,rand)
  13.160 +	| _ => u)
  13.161    in  abst(0,body)  end;
  13.162  
  13.163  
  13.164 @@ -388,16 +388,16 @@
  13.165  fun subst_atomic [] t = t : term
  13.166    | subst_atomic (instl: (term*term) list) t =
  13.167        let fun subst (Abs(a,T,body)) = Abs(a, T, subst body)
  13.168 -            | subst (f$t') = subst f $ subst t'
  13.169 -            | subst t = (case assoc(instl,t) of
  13.170 -                           Some u => u  |  None => t)
  13.171 +	    | subst (f$t') = subst f $ subst t'
  13.172 +	    | subst t = (case assoc(instl,t) of
  13.173 +		           Some u => u  |  None => t)
  13.174        in  subst t  end;
  13.175  
  13.176  (*Substitute for type Vars in a type*)
  13.177  fun typ_subst_TVars iTs T = if null iTs then T else
  13.178    let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
  13.179 -        | subst(T as TFree _) = T
  13.180 -        | subst(T as TVar(ixn,_)) =
  13.181 +	| subst(T as TFree _) = T
  13.182 +	| subst(T as TVar(ixn,_)) =
  13.183              (case assoc(iTs,ixn) of None => T | Some(U) => U)
  13.184    in subst T end;
  13.185  
  13.186 @@ -428,7 +428,7 @@
  13.187  
  13.188  (*Computing the maximum index of a typ*)
  13.189  fun maxidx_of_typ(Type(_,Ts)) =
  13.190 -        if Ts=[] then ~1 else max(map maxidx_of_typ Ts)
  13.191 +	if Ts=[] then ~1 else max(map maxidx_of_typ Ts)
  13.192    | maxidx_of_typ(TFree _) = ~1
  13.193    | maxidx_of_typ(TVar((_,i),_)) = i;
  13.194  
  13.195 @@ -457,10 +457,10 @@
  13.196    let val zero = ord"0"
  13.197        val limit = zero+radix
  13.198        fun scan (num,[]) = (num,[])
  13.199 -        | scan (num, c::cs) =
  13.200 -              if  zero <= ord c  andalso  ord c < limit
  13.201 -              then scan(radix*num + ord c - zero, cs)
  13.202 -              else (num, c::cs)
  13.203 +	| scan (num, c::cs) =
  13.204 +	      if  zero <= ord c  andalso  ord c < limit
  13.205 +	      then scan(radix*num + ord c - zero, cs)
  13.206 +	      else (num, c::cs)
  13.207    in  scan(0,cs)  end;
  13.208  
  13.209  fun scan_int cs = scan_radixint(10,cs);
  13.210 @@ -556,9 +556,9 @@
  13.211  fun insert_aterm (t,us) =
  13.212    let fun inserta [] = [t]
  13.213          | inserta (us as u::us') = 
  13.214 -              if atless(t,u) then t::us
  13.215 -              else if t=u then us (*duplicate*)
  13.216 -              else u :: inserta(us')
  13.217 +	      if atless(t,u) then t::us
  13.218 +	      else if t=u then us (*duplicate*)
  13.219 +	      else u :: inserta(us')
  13.220    in  inserta us  end;
  13.221  
  13.222  (*Accumulates the Vars in the term, suppressing duplicates*)
  13.223 @@ -588,7 +588,7 @@
  13.224  (* renames and reverses the strings in vars away from names *)
  13.225  fun rename_aTs names vars : (string*typ)list =
  13.226    let fun rename_aT (vars,(a,T)) =
  13.227 -                (variant (map #1 vars @ names) a, T) :: vars
  13.228 +		(variant (map #1 vars @ names) a, T) :: vars
  13.229    in foldl rename_aT ([],vars) end;
  13.230  
  13.231  fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
  13.232 @@ -618,18 +618,18 @@
  13.233  fun compress_type T =
  13.234    let val tag = type_tag T
  13.235        val tylist = the (Symtab.lookup (!memo_types, tag))
  13.236 -                   handle _ => []
  13.237 +	           handle _ => []
  13.238    in  
  13.239        case find_type (T,tylist) of
  13.240 -        Some T' => T'
  13.241 +	Some T' => T'
  13.242        | None => 
  13.243 -            let val T' =
  13.244 -                case T of
  13.245 -                    Type (a,Ts) => Type (a, map compress_type Ts)
  13.246 -                  | _ => T
  13.247 -            in  memo_types := Symtab.update ((tag, T'::tylist), !memo_types);
  13.248 -                T
  13.249 -            end
  13.250 +	    let val T' =
  13.251 +		case T of
  13.252 +		    Type (a,Ts) => Type (a, map compress_type Ts)
  13.253 +		  | _ => T
  13.254 +	    in  memo_types := Symtab.update ((tag, T'::tylist), !memo_types);
  13.255 +		T
  13.256 +	    end
  13.257    end
  13.258    handle Match =>
  13.259        let val Type (a,Ts) = T
  13.260 @@ -653,13 +653,13 @@
  13.261    | share_term (Abs (a,T,u)) = Abs (a, T, share_term u)
  13.262    | share_term t =
  13.263        let val tag = const_tag t
  13.264 -          val ts = the (Symtab.lookup (!memo_terms, tag))
  13.265 -                       handle _ => []
  13.266 +	  val ts = the (Symtab.lookup (!memo_terms, tag))
  13.267 +	               handle _ => []
  13.268        in 
  13.269 -          case find_term (t,ts) of
  13.270 -              Some t' => t'
  13.271 -            | None => (memo_terms := Symtab.update ((tag, t::ts), !memo_terms);
  13.272 -                       t)
  13.273 +	  case find_term (t,ts) of
  13.274 +	      Some t' => t'
  13.275 +	    | None => (memo_terms := Symtab.update ((tag, t::ts), !memo_terms);
  13.276 +		       t)
  13.277        end;
  13.278  
  13.279  val compress_term = share_term o map_term_types compress_type;
    14.1 --- a/src/Pure/thm.ML	Mon Jan 29 13:58:15 1996 +0100
    14.2 +++ b/src/Pure/thm.ML	Mon Jan 29 14:16:13 1996 +0100
    14.3 @@ -219,7 +219,7 @@
    14.4            Sign.infer_types sign types sorts used freeze (ts, T');
    14.5      val ct = cterm_of sign t'
    14.6        handle TYPE arg => error (Sign.exn_type_msg sign arg)
    14.7 -           | TERM (msg, _) => error msg;
    14.8 +	   | TERM (msg, _) => error msg;
    14.9    in (ct, tye) end;
   14.10  
   14.11  fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true;
   14.12 @@ -231,14 +231,14 @@
   14.13    let
   14.14      val {tsig, syn, ...} = Sign.rep_sg sign
   14.15      fun read (b,T) =
   14.16 -        case Syntax.read syn T b of
   14.17 -            [t] => t
   14.18 -          | _   => error("Error or ambiguity in parsing of " ^ b)
   14.19 +	case Syntax.read syn T b of
   14.20 +	    [t] => t
   14.21 +	  | _   => error("Error or ambiguity in parsing of " ^ b)
   14.22      val (us,_) = Type.infer_types(tsig, Sign.const_type sign, 
   14.23 -                                  K None, K None, 
   14.24 -                                  [], true, 
   14.25 -                                  map (Sign.certify_typ sign) Ts, 
   14.26 -                                  map read (bs~~Ts))
   14.27 +				  K None, K None, 
   14.28 +				  [], true, 
   14.29 +				  map (Sign.certify_typ sign) Ts, 
   14.30 +				  map read (bs~~Ts))
   14.31    in  map (cterm_of sign) us  end
   14.32    handle TYPE arg => error (Sign.exn_type_msg sign arg)
   14.33         | TERM (msg, _) => error msg;
   14.34 @@ -248,11 +248,11 @@
   14.35  (*** Meta theorems ***)
   14.36  
   14.37  datatype thm = Thm of
   14.38 -  {sign: Sign.sg,               (*signature for hyps and prop*)
   14.39 -   maxidx: int,                 (*maximum index of any Var or TVar*)
   14.40 -   shyps: sort list,            (* FIXME comment *)
   14.41 -   hyps: term list,             (*hypotheses*)
   14.42 -   prop: term};                 (*conclusion*)
   14.43 +  {sign: Sign.sg,		(*signature for hyps and prop*)
   14.44 +   maxidx: int,			(*maximum index of any Var or TVar*)
   14.45 +   shyps: sort list,		(* FIXME comment *)
   14.46 +   hyps: term list,		(*hypotheses*)
   14.47 +   prop: term};			(*conclusion*)
   14.48  
   14.49  fun rep_thm (Thm args) = args;
   14.50  
   14.51 @@ -335,10 +335,10 @@
   14.52    as it could be slow.*)
   14.53  fun compress (Thm {sign, maxidx, shyps, hyps, prop}) = 
   14.54      Thm {sign = sign, 
   14.55 -         maxidx = maxidx,
   14.56 -         shyps = shyps, 
   14.57 -         hyps = map Term.compress_term hyps, 
   14.58 -         prop = Term.compress_term prop};
   14.59 +	 maxidx = maxidx,
   14.60 +	 shyps = shyps, 
   14.61 +	 hyps = map Term.compress_term hyps, 
   14.62 +	 prop = Term.compress_term prop};
   14.63  
   14.64  
   14.65  (* fix_shyps *)
   14.66 @@ -518,7 +518,7 @@
   14.67    let
   14.68      val Cterm {t, T, ...} = cterm_of sg raw_tm
   14.69        handle TYPE arg => error (Sign.exn_type_msg sg arg)
   14.70 -           | TERM (msg, _) => error msg;
   14.71 +	   | TERM (msg, _) => error msg;
   14.72    in
   14.73      assert (T = propT) "Term not of type prop";
   14.74      (name, no_vars t)
   14.75 @@ -542,8 +542,8 @@
   14.76    let
   14.77      val sign1 = Sign.make_draft sign;
   14.78      val axioms = map (apsnd (Term.compress_term o Logic.varify) o 
   14.79 -                      prep_axm sign) 
   14.80 -                 axms;
   14.81 +		      prep_axm sign) 
   14.82 +	         axms;
   14.83    in
   14.84      ext_thy thy sign1 axioms
   14.85    end;
    15.1 --- a/src/Pure/type.ML	Mon Jan 29 13:58:15 1996 +0100
    15.2 +++ b/src/Pure/type.ML	Mon Jan 29 14:16:13 1996 +0100
    15.3 @@ -904,7 +904,7 @@
    15.4                  val (T, tyeT) = inf(Ts, f, tyeU);
    15.5                  fun err s =
    15.6                    raise TYPE(s, [inst_typ tyeT T, inst_typ tyeT U], [f$u])
    15.7 -                val msg = "function type is incompatible with argument type"
    15.8 +		val msg = "function type is incompatible with argument type"
    15.9              in case T of
   15.10                   Type("fun", [T1, T2]) =>
   15.11                     ( (T2, unify1 tsig ((T1, U), tyeT))
   15.12 @@ -1049,7 +1049,7 @@
   15.13  
   15.14  
   15.15  (*Infer types for terms.  Given Ts=[T1,...,Tn] and ts=[t1,...,tn], ensure that
   15.16 -        the type of ti unifies with Ti (i=1,...,n).
   15.17 +	the type of ti unifies with Ti (i=1,...,n).
   15.18    types is a partial map from indexnames to types (constrains Free, Var).
   15.19    sorts is a partial map from indexnames to sorts (constrains TFree, TVar).
   15.20    used is the list of already used type variables.
    16.1 --- a/src/Pure/unify.ML	Mon Jan 29 13:58:15 1996 +0100
    16.2 +++ b/src/Pure/unify.ML	Mon Jan 29 14:16:13 1996 +0100
    16.3 @@ -1,6 +1,6 @@
    16.4 -(*  Title:      unify
    16.5 +(*  Title: 	unify
    16.6      ID:         $Id$
    16.7 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    16.8 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    16.9      Copyright   Cambridge University 1992
   16.10  
   16.11  Higher-Order Unification
   16.12 @@ -28,16 +28,16 @@
   16.13    val combound : (term*int*int) -> term
   16.14    val rlist_abs: (string*typ)list * term -> term   
   16.15    val smash_unifiers : Sign.sg * Envir.env * (term*term)list
   16.16 -        -> (Envir.env Sequence.seq)
   16.17 +	-> (Envir.env Sequence.seq)
   16.18    val unifiers: Sign.sg * Envir.env * ((term*term)list)
   16.19 -        -> (Envir.env * (term * term)list) Sequence.seq
   16.20 +	-> (Envir.env * (term * term)list) Sequence.seq
   16.21  end;
   16.22  
   16.23  functor UnifyFun (structure Sign: SIGN and Envir: ENVIR and Sequence: SEQUENCE
   16.24                    and Pattern:PATTERN
   16.25                    sharing type Sign.sg = Pattern.sg
   16.26                    and     type Envir.env = Pattern.env)
   16.27 -        : UNIFY = 
   16.28 +	: UNIFY = 
   16.29  struct
   16.30  
   16.31  structure Sign = Sign;
   16.32 @@ -47,11 +47,11 @@
   16.33  
   16.34  (*Unification options*)
   16.35  
   16.36 -val trace_bound = ref 10        (*tracing starts above this depth, 0 for full*)
   16.37 -and search_bound = ref 20       (*unification quits above this depth*)
   16.38 -and trace_simp = ref false      (*print dpairs before calling SIMPL*)
   16.39 -and trace_types = ref false     (*announce potential incompleteness
   16.40 -                                  of type unification*)
   16.41 +val trace_bound = ref 10	(*tracing starts above this depth, 0 for full*)
   16.42 +and search_bound = ref 20	(*unification quits above this depth*)
   16.43 +and trace_simp = ref false	(*print dpairs before calling SIMPL*)
   16.44 +and trace_types = ref false	(*announce potential incompleteness
   16.45 +				  of type unification*)
   16.46  
   16.47  val sgr = ref(Sign.proto_pure);
   16.48  
   16.49 @@ -62,14 +62,14 @@
   16.50  fun body_type(Envir.Envir{iTs,...}) = 
   16.51  let fun bT(Type("fun",[_,T])) = bT T
   16.52        | bT(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
   16.53 -                None => T | Some(T') => bT T')
   16.54 +		None => T | Some(T') => bT T')
   16.55        | bT T = T
   16.56  in bT end;
   16.57  
   16.58  fun binder_types(Envir.Envir{iTs,...}) = 
   16.59  let fun bTs(Type("fun",[T,U])) = T :: bTs U
   16.60        | bTs(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
   16.61 -                None => [] | Some(T') => bTs T')
   16.62 +		None => [] | Some(T') => bTs T')
   16.63        | bTs _ = []
   16.64  in bTs end;
   16.65  
   16.66 @@ -82,7 +82,7 @@
   16.67    inefficiency, avoid partial application:  if an atom is applied to
   16.68    any arguments at all, apply it to its full number of arguments.
   16.69    For
   16.70 -    rbinder = [(x1,T),...,(xm,Tm)]              (user's var names preserved!)
   16.71 +    rbinder = [(x1,T),...,(xm,Tm)]		(user's var names preserved!)
   16.72      args  =   [arg1,...,argn]
   16.73    the value of 
   16.74        (xm,...,x1)(head(arg1,...,argn))  remains invariant.
   16.75 @@ -92,18 +92,18 @@
   16.76  in
   16.77    fun head_norm (env,t) : term =
   16.78      let fun hnorm (Var (v,T)) = 
   16.79 -              (case Envir.lookup (env,v) of
   16.80 -                  Some u => head_norm (env, u)
   16.81 -                | None   => raise SAME)
   16.82 -          | hnorm (Abs(a,T,body)) =  Abs(a, T, hnorm body)
   16.83 -          | hnorm (Abs(_,_,body) $ t) =
   16.84 -              head_norm (env, subst_bounds([t], body))
   16.85 -          | hnorm (f $ t) =
   16.86 -              (case hnorm f of
   16.87 -                 Abs(_,_,body) =>
   16.88 -                   head_norm (env, subst_bounds([t], body))
   16.89 -               | nf => nf $ t)
   16.90 -          | hnorm _ =  raise SAME
   16.91 +	      (case Envir.lookup (env,v) of
   16.92 +		  Some u => head_norm (env, u)
   16.93 +		| None   => raise SAME)
   16.94 +	  | hnorm (Abs(a,T,body)) =  Abs(a, T, hnorm body)
   16.95 +	  | hnorm (Abs(_,_,body) $ t) =
   16.96 +	      head_norm (env, subst_bounds([t], body))
   16.97 +	  | hnorm (f $ t) =
   16.98 +	      (case hnorm f of
   16.99 +		 Abs(_,_,body) =>
  16.100 +		   head_norm (env, subst_bounds([t], body))
  16.101 +	       | nf => nf $ t)
  16.102 +	  | hnorm _ =  raise SAME
  16.103      in  hnorm t  handle SAME=> t  end
  16.104  end;
  16.105  
  16.106 @@ -113,18 +113,18 @@
  16.107  fun fastype (Envir.Envir{iTs,...}) =
  16.108  let val funerr = "fastype: expected function type";
  16.109      fun fast(rbinder, f$u) =
  16.110 -        (case (fast (rbinder, f)) of
  16.111 -           Type("fun",[_,T]) => T
  16.112 -         | TVar(ixn,_) =>
  16.113 -                (case assoc(iTs,ixn) of
  16.114 -                   Some(Type("fun",[_,T])) => T
  16.115 -                 | _ => raise TERM(funerr, [f$u]))
  16.116 -         | _ => raise TERM(funerr, [f$u]))
  16.117 +	(case (fast (rbinder, f)) of
  16.118 +	   Type("fun",[_,T]) => T
  16.119 +	 | TVar(ixn,_) =>
  16.120 +		(case assoc(iTs,ixn) of
  16.121 +		   Some(Type("fun",[_,T])) => T
  16.122 +		 | _ => raise TERM(funerr, [f$u]))
  16.123 +	 | _ => raise TERM(funerr, [f$u]))
  16.124        | fast (rbinder, Const (_,T)) = T
  16.125        | fast (rbinder, Free (_,T)) = T
  16.126        | fast (rbinder, Bound i) =
  16.127 -        (#2 (nth_elem (i,rbinder))
  16.128 -         handle LIST _=> raise TERM("fastype: Bound", [Bound i]))
  16.129 +	(#2 (nth_elem (i,rbinder))
  16.130 +  	 handle LIST _=> raise TERM("fastype: Bound", [Bound i]))
  16.131        | fast (rbinder, Var (_,T)) = T 
  16.132        | fast (rbinder, Abs (_,T,u)) =  T --> fast (("",T) :: rbinder, u)
  16.133  in fast end;
  16.134 @@ -133,14 +133,14 @@
  16.135  (*Eta normal form*)
  16.136  fun eta_norm(env as Envir.Envir{iTs,...}) =
  16.137    let fun etif (Type("fun",[T,U]), t) =
  16.138 -            Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
  16.139 -        | etif (TVar(ixn,_),t) = 
  16.140 -            (case assoc(iTs,ixn) of
  16.141 -                  None => t | Some(T) => etif(T,t))
  16.142 -        | etif (_,t) = t;
  16.143 +	    Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
  16.144 +	| etif (TVar(ixn,_),t) = 
  16.145 +	    (case assoc(iTs,ixn) of
  16.146 +		  None => t | Some(T) => etif(T,t))
  16.147 +	| etif (_,t) = t;
  16.148        fun eta_nm (rbinder, Abs(a,T,body)) =
  16.149 -            Abs(a, T, eta_nm ((a,T)::rbinder, body))
  16.150 -        | eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
  16.151 +	    Abs(a, T, eta_nm ((a,T)::rbinder, body))
  16.152 +	| eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
  16.153    in eta_nm end;
  16.154  
  16.155  
  16.156 @@ -150,22 +150,22 @@
  16.157    "seen" is list of variables passed thru, is a memo variable for sharing.
  16.158    This version searches for nonrigid occurrence, returns true if found. *)
  16.159  fun occurs_terms (seen: (indexname list) ref,
  16.160 -                  env: Envir.env, v: indexname, ts: term list): bool =
  16.161 + 		  env: Envir.env, v: indexname, ts: term list): bool =
  16.162    let fun occurs [] = false
  16.163 -        | occurs (t::ts) =  occur t  orelse  occurs ts
  16.164 +	| occurs (t::ts) =  occur t  orelse  occurs ts
  16.165        and occur (Const _)  = false
  16.166 -        | occur (Bound _)  = false
  16.167 -        | occur (Free _)  = false
  16.168 -        | occur (Var (w,_))  = 
  16.169 -            if w mem !seen then false
  16.170 -            else if v=w then true
  16.171 -              (*no need to lookup: v has no assignment*)
  16.172 -            else (seen := w:: !seen;  
  16.173 -                  case  Envir.lookup(env,w)  of
  16.174 -                      None    => false
  16.175 -                    | Some t => occur t)
  16.176 -        | occur (Abs(_,_,body)) = occur body
  16.177 -        | occur (f$t) = occur t  orelse   occur f
  16.178 +	| occur (Bound _)  = false
  16.179 +	| occur (Free _)  = false
  16.180 +	| occur (Var (w,_))  = 
  16.181 +	    if w mem !seen then false
  16.182 +	    else if v=w then true
  16.183 +	      (*no need to lookup: v has no assignment*)
  16.184 +	    else (seen := w:: !seen;  
  16.185 +	          case  Envir.lookup(env,w)  of
  16.186 +		      None    => false
  16.187 +		    | Some t => occur t)
  16.188 +	| occur (Abs(_,_,body)) = occur body
  16.189 +	| occur (f$t) = occur t  orelse   occur f
  16.190    in  occurs ts  end;
  16.191  
  16.192  
  16.193 @@ -174,7 +174,7 @@
  16.194  fun head_of_in (env,t) : term = case t of
  16.195      f$_ => head_of_in(env,f)
  16.196    | Var (v,_) => (case  Envir.lookup(env,v)  of  
  16.197 -                        Some u => head_of_in(env,u)  |  None   => t)
  16.198 +			Some u => head_of_in(env,u)  |  None   => t)
  16.199    | _ => t;
  16.200  
  16.201  
  16.202 @@ -205,9 +205,9 @@
  16.203  *)
  16.204  fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) = 
  16.205    let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid 
  16.206 -                       else NoOcc
  16.207 +		       else NoOcc
  16.208        fun occurs [] = NoOcc
  16.209 -        | occurs (t::ts) =
  16.210 +	| occurs (t::ts) =
  16.211              (case occur t of
  16.212                 Rigid => Rigid
  16.213               | oc =>  (case occurs ts of NoOcc => oc  |  oc2 => oc2))
  16.214 @@ -217,28 +217,28 @@
  16.215               | oc =>  (case occomb f of NoOcc => oc  |  oc2 => oc2))
  16.216          | occomb t = occur t
  16.217        and occur (Const _)  = NoOcc
  16.218 -        | occur (Bound _)  = NoOcc
  16.219 -        | occur (Free _)  = NoOcc
  16.220 -        | occur (Var (w,_))  = 
  16.221 -            if w mem !seen then NoOcc
  16.222 -            else if v=w then Rigid
  16.223 -            else (seen := w:: !seen;  
  16.224 -                  case  Envir.lookup(env,w)  of
  16.225 -                      None    => NoOcc
  16.226 -                    | Some t => occur t)
  16.227 -        | occur (Abs(_,_,body)) = occur body
  16.228 -        | occur (t as f$_) =  (*switch to nonrigid search?*)
  16.229 -           (case head_of_in (env,f) of
  16.230 -              Var (w,_) => (*w is not assigned*)
  16.231 -                if v=w then Rigid  
  16.232 -                else  nonrigid t
  16.233 -            | Abs(_,_,body) => nonrigid t (*not in normal form*)
  16.234 -            | _ => occomb t)
  16.235 +	| occur (Bound _)  = NoOcc
  16.236 +	| occur (Free _)  = NoOcc
  16.237 +	| occur (Var (w,_))  = 
  16.238 +	    if w mem !seen then NoOcc
  16.239 +	    else if v=w then Rigid
  16.240 +	    else (seen := w:: !seen;  
  16.241 +	          case  Envir.lookup(env,w)  of
  16.242 +		      None    => NoOcc
  16.243 +		    | Some t => occur t)
  16.244 +	| occur (Abs(_,_,body)) = occur body
  16.245 +	| occur (t as f$_) =  (*switch to nonrigid search?*)
  16.246 +	   (case head_of_in (env,f) of
  16.247 +	      Var (w,_) => (*w is not assigned*)
  16.248 +		if v=w then Rigid  
  16.249 +		else  nonrigid t
  16.250 +	    | Abs(_,_,body) => nonrigid t (*not in normal form*)
  16.251 +	    | _ => occomb t)
  16.252    in  occur t  end;
  16.253  
  16.254  
  16.255 -exception CANTUNIFY;    (*Signals non-unifiability.  Does not signal errors!*)
  16.256 -exception ASSIGN;       (*Raised if not an assignment*)
  16.257 +exception CANTUNIFY;	(*Signals non-unifiability.  Does not signal errors!*)
  16.258 +exception ASSIGN;	(*Raised if not an assignment*)
  16.259  
  16.260  
  16.261  fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
  16.262 @@ -261,8 +261,8 @@
  16.263    Result is var a for use in SIMPL. *)
  16.264  fun get_eta_var ([], _, Var vT)  =  vT
  16.265    | get_eta_var (_::rbinder, n, f $ Bound i) =
  16.266 -        if  n=i  then  get_eta_var (rbinder, n+1, f) 
  16.267 -                 else  raise ASSIGN
  16.268 +	if  n=i  then  get_eta_var (rbinder, n+1, f) 
  16.269 +		 else  raise ASSIGN
  16.270    | get_eta_var _ = raise ASSIGN;
  16.271  
  16.272  
  16.273 @@ -277,11 +277,11 @@
  16.274  fun assignment (env, rbinder, t, u) =
  16.275      let val (v,T) = get_eta_var(rbinder,0,t)
  16.276      in  case rigid_occurs_term (ref[], env, v, u) of
  16.277 -              NoOcc => let val env = unify_types(body_type env T,
  16.278 -                                                 fastype env (rbinder,u),env)
  16.279 -                in Envir.update ((v, rlist_abs(rbinder,u)), env) end
  16.280 -            | Nonrigid =>  raise ASSIGN
  16.281 -            | Rigid =>  raise CANTUNIFY
  16.282 +	      NoOcc => let val env = unify_types(body_type env T,
  16.283 +						 fastype env (rbinder,u),env)
  16.284 +		in Envir.update ((v, rlist_abs(rbinder,u)), env) end
  16.285 +	    | Nonrigid =>  raise ASSIGN
  16.286 +	    | Rigid =>  raise CANTUNIFY
  16.287      end;
  16.288  
  16.289  
  16.290 @@ -291,9 +291,9 @@
  16.291      if not, raises TERM, probably indicating type mismatch.
  16.292    Uses variable a (unless the null string) to preserve user's naming.*) 
  16.293  fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
  16.294 -        let val env' = unify_types(T,U,env)
  16.295 -            val c = if a="" then b else a
  16.296 -        in new_dpair((c,T) :: rbinder, body1, body2, env') end
  16.297 +	let val env' = unify_types(T,U,env)
  16.298 +	    val c = if a="" then b else a
  16.299 +	in new_dpair((c,T) :: rbinder, body1, body2, env') end
  16.300      | new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", [])
  16.301      | new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", [])
  16.302      | new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
  16.303 @@ -301,8 +301,8 @@
  16.304  
  16.305  fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
  16.306       new_dpair (rbinder,
  16.307 -                eta_norm env (rbinder, head_norm(env,t)),
  16.308 -                eta_norm env (rbinder, head_norm(env,u)), env);
  16.309 +		eta_norm env (rbinder, head_norm(env,t)),
  16.310 +	  	eta_norm env (rbinder, head_norm(env,u)), env);
  16.311  
  16.312  
  16.313  
  16.314 @@ -313,34 +313,34 @@
  16.315      do so caused numerous problems with no compensating advantage.
  16.316  *)
  16.317  fun SIMPL0 (dp0, (env,flexflex,flexrigid))
  16.318 -        : Envir.env * dpair list * dpair list =
  16.319 +	: Envir.env * dpair list * dpair list =
  16.320      let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);
  16.321 -            fun SIMRANDS(f$t, g$u, env) =
  16.322 -                        SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
  16.323 -              | SIMRANDS (t as _$_, _, _) =
  16.324 -                raise TERM ("SIMPL: operands mismatch", [t,u])
  16.325 -              | SIMRANDS (t, u as _$_, _) =
  16.326 -                raise TERM ("SIMPL: operands mismatch", [t,u])
  16.327 -              | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
  16.328 +	    fun SIMRANDS(f$t, g$u, env) =
  16.329 +			SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
  16.330 +	      | SIMRANDS (t as _$_, _, _) =
  16.331 +		raise TERM ("SIMPL: operands mismatch", [t,u])
  16.332 +	      | SIMRANDS (t, u as _$_, _) =
  16.333 +		raise TERM ("SIMPL: operands mismatch", [t,u])
  16.334 +	      | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
  16.335      in case (head_of t, head_of u) of
  16.336         (Var(_,T), Var(_,U)) =>
  16.337 -            let val T' = body_type env T and U' = body_type env U;
  16.338 -                val env = unify_types(T',U',env)
  16.339 -            in (env, dp::flexflex, flexrigid) end
  16.340 +	    let val T' = body_type env T and U' = body_type env U;
  16.341 +		val env = unify_types(T',U',env)
  16.342 +	    in (env, dp::flexflex, flexrigid) end
  16.343       | (Var _, _) =>
  16.344 -            ((assignment (env,rbinder,t,u), flexflex, flexrigid)
  16.345 -             handle ASSIGN => (env, flexflex, dp::flexrigid))
  16.346 +	    ((assignment (env,rbinder,t,u), flexflex, flexrigid)
  16.347 +	     handle ASSIGN => (env, flexflex, dp::flexrigid))
  16.348       | (_, Var _) =>
  16.349 -            ((assignment (env,rbinder,u,t), flexflex, flexrigid)
  16.350 -             handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
  16.351 +	    ((assignment (env,rbinder,u,t), flexflex, flexrigid)
  16.352 +	     handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
  16.353       | (Const(a,T), Const(b,U)) =>
  16.354 -            if a=b then SIMRANDS(t,u, unify_types(T,U,env))
  16.355 -            else raise CANTUNIFY
  16.356 +	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
  16.357 +	    else raise CANTUNIFY
  16.358       | (Bound i,    Bound j)    =>
  16.359 -            if i=j  then SIMRANDS(t,u,env) else raise CANTUNIFY
  16.360 +	    if i=j  then SIMRANDS(t,u,env) else raise CANTUNIFY
  16.361       | (Free(a,T),  Free(b,U))  =>
  16.362 -            if a=b then SIMRANDS(t,u, unify_types(T,U,env))
  16.363 -            else raise CANTUNIFY
  16.364 +	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
  16.365 +	    else raise CANTUNIFY
  16.366       | _ => raise CANTUNIFY
  16.367      end;
  16.368  
  16.369 @@ -356,8 +356,8 @@
  16.370    Clever would be to re-do just the affected dpairs*)
  16.371  fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
  16.372      let val all as (env',flexflex,flexrigid) =
  16.373 -            foldr SIMPL0 (dpairs, (env,[],[]));
  16.374 -        val dps = flexrigid@flexflex
  16.375 +	    foldr SIMPL0 (dpairs, (env,[],[]));
  16.376 +	val dps = flexrigid@flexflex
  16.377      in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
  16.378         then SIMPL(env',dps) else all
  16.379      end;
  16.380 @@ -376,7 +376,7 @@
  16.381  fun make_args name (binder: typ list, env, []) = (env, [])   (*frequent case*)
  16.382    | make_args name (binder: typ list, env, Ts) : Envir.env * term list =
  16.383         let fun funtype T = binder--->T;
  16.384 -           val (env', vars) = Envir.genvars name (env, map funtype Ts)
  16.385 +	   val (env', vars) = Envir.genvars name (env, map funtype Ts)
  16.386         in  (env',  map (fn var=> combound(var, 0, length binder)) vars)  end;
  16.387  
  16.388  
  16.389 @@ -398,60 +398,60 @@
  16.390    The order for trying projections is crucial in ?b'(?a)   
  16.391    NB "vname" is only used in the call to make_args!!   *)
  16.392  fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 
  16.393 -        : (term * (Envir.env * dpair list))Sequence.seq =
  16.394 +	: (term * (Envir.env * dpair list))Sequence.seq =
  16.395  let (*Produce copies of uarg and cons them in front of uargs*)
  16.396      fun copycons uarg (uargs, (env, dpairs)) =
  16.397 -        Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed'))
  16.398 -            (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
  16.399 -                 (env, dpairs)));
  16.400 -        (*Produce sequence of all possible ways of copying the arg list*)
  16.401 +	Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed'))
  16.402 +	    (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
  16.403 +		 (env, dpairs)));
  16.404 +	(*Produce sequence of all possible ways of copying the arg list*)
  16.405      fun copyargs [] = Sequence.cons( ([],ed), Sequence.null)
  16.406        | copyargs (uarg::uargs) =
  16.407 -            Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs));
  16.408 +	    Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs));
  16.409      val (uhead,uargs) = strip_comb u;
  16.410      val base = body_type env (fastype env (rbinder,uhead));
  16.411      fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
  16.412      (*attempt projection on argument with given typ*)
  16.413      val Ts = map (curry (fastype env) rbinder) targs;
  16.414      fun projenv (head, (Us,bary), targ, tail) = 
  16.415 -        let val env = if !trace_types then test_unify_types(base,bary,env)
  16.416 -                      else unify_types(base,bary,env)
  16.417 -        in Sequence.seqof (fn () =>  
  16.418 -            let val (env',args) = make_args vname (Ts,env,Us);
  16.419 -                (*higher-order projection: plug in targs for bound vars*)
  16.420 -                fun plugin arg = list_comb(head_of arg, targs);
  16.421 -                val dp = (rbinder, list_comb(targ, map plugin args), u);
  16.422 -                val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
  16.423 -                    (*may raise exception CANTUNIFY*)
  16.424 -            in  Some ((list_comb(head,args), (env2, frigid@fflex)),
  16.425 -                        tail)
  16.426 -            end  handle CANTUNIFY => Sequence.pull tail)
  16.427 -        end handle CANTUNIFY => tail;
  16.428 +	let val env = if !trace_types then test_unify_types(base,bary,env)
  16.429 +		      else unify_types(base,bary,env)
  16.430 +	in Sequence.seqof (fn () =>  
  16.431 +	    let val (env',args) = make_args vname (Ts,env,Us);
  16.432 +		(*higher-order projection: plug in targs for bound vars*)
  16.433 +		fun plugin arg = list_comb(head_of arg, targs);
  16.434 +		val dp = (rbinder, list_comb(targ, map plugin args), u);
  16.435 +		val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
  16.436 +		    (*may raise exception CANTUNIFY*)
  16.437 +	    in  Some ((list_comb(head,args), (env2, frigid@fflex)),
  16.438 +			tail)
  16.439 +	    end  handle CANTUNIFY => Sequence.pull tail)
  16.440 +	end handle CANTUNIFY => tail;
  16.441      (*make a list of projections*)
  16.442      fun make_projs (T::Ts, targ::targs) =
  16.443 -              (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
  16.444 +	      (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
  16.445        | make_projs ([],[]) = []
  16.446        | make_projs _ = raise TERM ("make_projs", u::targs);
  16.447      (*try projections and imitation*)
  16.448      fun matchfun ((bvar,T,targ)::projs) =
  16.449 -               (projenv(bvar, strip_type env T, targ, matchfun projs))
  16.450 +	       (projenv(bvar, strip_type env T, targ, matchfun projs))
  16.451        | matchfun [] = (*imitation last of all*)
  16.452 -              (case uhead of
  16.453 -                 Const _ => Sequence.maps joinargs (copyargs uargs)
  16.454 -               | Free _  => Sequence.maps joinargs (copyargs uargs)
  16.455 -               | _ => Sequence.null)  (*if Var, would be a loop!*)
  16.456 +	      (case uhead of
  16.457 +		 Const _ => Sequence.maps joinargs (copyargs uargs)
  16.458 +	       | Free _  => Sequence.maps joinargs (copyargs uargs)
  16.459 +	       | _ => Sequence.null)  (*if Var, would be a loop!*)
  16.460  in case uhead of
  16.461 -        Abs(a, T, body) =>
  16.462 -            Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed')) 
  16.463 -                (mc ((a,T)::rbinder,
  16.464 -                        (map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
  16.465 +	Abs(a, T, body) =>
  16.466 +	    Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed')) 
  16.467 +		(mc ((a,T)::rbinder,
  16.468 +			(map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
  16.469        | Var (w,uary) => 
  16.470 -            (*a flex-flex dpair: make variable for t*)
  16.471 -            let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
  16.472 -                val tabs = combound(newhd, 0, length Ts)
  16.473 -                val tsub = list_comb(newhd,targs)
  16.474 -            in  Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
  16.475 -            end
  16.476 +	    (*a flex-flex dpair: make variable for t*)
  16.477 +	    let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
  16.478 +		val tabs = combound(newhd, 0, length Ts)
  16.479 +		val tsub = list_comb(newhd,targs)
  16.480 +	    in  Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
  16.481 +	    end
  16.482        | _ =>  matchfun(rev(make_projs(Ts, targs)))
  16.483  end
  16.484  in mc end;
  16.485 @@ -459,14 +459,14 @@
  16.486  
  16.487  (*Call matchcopy to produce assignments to the variable in the dpair*)
  16.488  fun MATCH (env, (rbinder,t,u), dpairs)
  16.489 -        : (Envir.env * dpair list)Sequence.seq = 
  16.490 +	: (Envir.env * dpair list)Sequence.seq = 
  16.491    let val (Var(v,T), targs) = strip_comb t;
  16.492        val Ts = binder_types env T;
  16.493        fun new_dset (u', (env',dpairs')) =
  16.494 -          (*if v was updated to s, must unify s with u' *)
  16.495 -          case Envir.lookup(env',v) of
  16.496 -              None => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
  16.497 -            | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
  16.498 +	  (*if v was updated to s, must unify s with u' *)
  16.499 +	  case Envir.lookup(env',v) of
  16.500 +	      None => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
  16.501 +	    | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
  16.502    in Sequence.maps new_dset
  16.503           (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
  16.504    end;
  16.505 @@ -481,9 +481,9 @@
  16.506  let val (v,T) = get_eta_var(rbinder,0,t)
  16.507  in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN
  16.508     else let val env = unify_types(body_type env T,
  16.509 -                                  fastype env (rbinder,u),
  16.510 -                                  env)
  16.511 -        in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
  16.512 +				  fastype env (rbinder,u),
  16.513 +				  env)
  16.514 +	in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
  16.515  end;
  16.516  
  16.517  
  16.518 @@ -508,30 +508,30 @@
  16.519    let val (head,args) = strip_comb t 
  16.520    in  
  16.521        case head of
  16.522 -          Bound i => (i-lev) mem banned  orelse
  16.523 -                     exists (rigid_bound (lev, banned)) args
  16.524 -        | Var _ => false        (*no rigid occurrences here!*)
  16.525 -        | Abs (_,_,u) => 
  16.526 -               rigid_bound(lev+1, banned) u  orelse
  16.527 -               exists (rigid_bound (lev, banned)) args
  16.528 -        | _ => exists (rigid_bound (lev, banned)) args
  16.529 +	  Bound i => (i-lev) mem banned  orelse
  16.530 +	      	     exists (rigid_bound (lev, banned)) args
  16.531 +	| Var _ => false	(*no rigid occurrences here!*)
  16.532 +	| Abs (_,_,u) => 
  16.533 +	       rigid_bound(lev+1, banned) u  orelse
  16.534 +	       exists (rigid_bound (lev, banned)) args
  16.535 +	| _ => exists (rigid_bound (lev, banned)) args
  16.536    end;
  16.537  
  16.538  (*Squash down indices at level >=lev to delete the banned from a term.*)
  16.539  fun change_bnos banned =
  16.540    let fun change lev (Bound i) = 
  16.541 -            if i<lev then Bound i
  16.542 -            else  if (i-lev) mem banned  
  16.543 -                  then raise CHANGE_FAIL (**flexible occurrence: give up**)
  16.544 -            else  Bound (i - length (filter (fn j => j < i-lev) banned))
  16.545 -        | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
  16.546 -        | change lev (t$u) = change lev t $ change lev u
  16.547 -        | change lev t = t
  16.548 +	    if i<lev then Bound i
  16.549 +	    else  if (i-lev) mem banned  
  16.550 +		  then raise CHANGE_FAIL (**flexible occurrence: give up**)
  16.551 +	    else  Bound (i - length (filter (fn j => j < i-lev) banned))
  16.552 +	| change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
  16.553 +	| change lev (t$u) = change lev t $ change lev u
  16.554 +	| change lev t = t
  16.555    in  change 0  end;
  16.556  
  16.557  (*Change indices, delete the argument if it contains a banned Bound*)
  16.558  fun change_arg banned ({j,t,T}, args) : flarg list =
  16.559 -    if rigid_bound (0, banned) t  then  args    (*delete argument!*)
  16.560 +    if rigid_bound (0, banned) t  then  args	(*delete argument!*)
  16.561      else  {j=j, t= change_bnos banned t, T=T} :: args;
  16.562  
  16.563  
  16.564 @@ -550,19 +550,19 @@
  16.565    Update its head; squash indices in arguments. *)
  16.566  fun clean_term banned (env,t) =
  16.567      let val (Var(v,T), ts) = strip_comb t
  16.568 -        val (Ts,U) = strip_type env T
  16.569 -        and js = length ts - 1  downto 0
  16.570 -        val args = sort arg_less
  16.571 -                (foldr (change_arg banned) (flexargs (js,ts,Ts), []))
  16.572 -        val ts' = map (#t) args
  16.573 +	val (Ts,U) = strip_type env T
  16.574 +	and js = length ts - 1  downto 0
  16.575 +	val args = sort arg_less
  16.576 +		(foldr (change_arg banned) (flexargs (js,ts,Ts), []))
  16.577 +	val ts' = map (#t) args
  16.578      in
  16.579      if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
  16.580      else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
  16.581 -             val body = list_comb(v', map (Bound o #j) args)
  16.582 -             val env2 = Envir.vupdate (((v, types_abs(Ts, body)),   env'))
  16.583 -             (*the vupdate affects ts' if they contain v*)
  16.584 -         in  
  16.585 -             (env2, Envir.norm_term env2 (list_comb(v',ts')))
  16.586 +	     val body = list_comb(v', map (Bound o #j) args)
  16.587 +	     val env2 = Envir.vupdate (((v, types_abs(Ts, body)),   env'))
  16.588 +	     (*the vupdate affects ts' if they contain v*)
  16.589 +	 in  
  16.590 +	     (env2, Envir.norm_term env2 (list_comb(v',ts')))
  16.591           end
  16.592      end;
  16.593  
  16.594 @@ -583,8 +583,8 @@
  16.595    let val loot = loose_bnos t  and  loou = loose_bnos u
  16.596        fun add_index (((a,T), j), (bnos, newbinder)) = 
  16.597              if  j mem loot  andalso  j mem loou 
  16.598 -            then  (bnos, (a,T)::newbinder)      (*needed by both: keep*)
  16.599 -            else  (j::bnos, newbinder);         (*remove*)
  16.600 +            then  (bnos, (a,T)::newbinder)	(*needed by both: keep*)
  16.601 +            else  (j::bnos, newbinder);		(*remove*)
  16.602        val indices = 0 upto (length rbinder - 1);
  16.603        val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[]));
  16.604        val (env', t') = clean_term banned (env, t);
  16.605 @@ -605,11 +605,11 @@
  16.606    let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
  16.607    in  case  (head_of t, head_of u) of
  16.608        (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
  16.609 -        if v=w then             (*...occur check would falsely return true!*)
  16.610 -            if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
  16.611 -            else raise TERM ("add_ffpair: Var name confusion", [t,u])
  16.612 -        else if xless(v,w) then (*prefer to update the LARGER variable*)
  16.613 -             clean_ffpair ((rbinder, u, t), (env,tpairs))
  16.614 +	if v=w then		(*...occur check would falsely return true!*)
  16.615 +	    if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
  16.616 +	    else raise TERM ("add_ffpair: Var name confusion", [t,u])
  16.617 +	else if xless(v,w) then (*prefer to update the LARGER variable*)
  16.618 +	     clean_ffpair ((rbinder, u, t), (env,tpairs))
  16.619          else clean_ffpair ((rbinder, t, u), (env,tpairs))
  16.620      | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
  16.621    end;
  16.622 @@ -634,26 +634,26 @@
  16.623  fun hounifiers (sg,env, tus : (term*term)list) 
  16.624    : (Envir.env * (term*term)list)Sequence.seq =
  16.625    let fun add_unify tdepth ((env,dpairs), reseq) =
  16.626 -          Sequence.seqof (fn()=>
  16.627 -          let val (env',flexflex,flexrigid) = 
  16.628 -               (if tdepth> !trace_bound andalso !trace_simp
  16.629 -                then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
  16.630 -                SIMPL (env,dpairs))
  16.631 -          in case flexrigid of
  16.632 -              [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
  16.633 -            | dp::frigid' => 
  16.634 -                if tdepth > !search_bound then
  16.635 -                    (prs"***Unification bound exceeded\n"; Sequence.pull reseq)
  16.636 -                else
  16.637 -                (if tdepth > !trace_bound then
  16.638 -                    print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
  16.639 -                 else ();
  16.640 -                 Sequence.pull (Sequence.its_right (add_unify (tdepth+1))
  16.641 -                           (MATCH (env',dp, frigid'@flexflex), reseq)))
  16.642 -          end
  16.643 -          handle CANTUNIFY => 
  16.644 -            (if tdepth > !trace_bound then writeln"Failure node" else ();
  16.645 -             Sequence.pull reseq));
  16.646 +	  Sequence.seqof (fn()=>
  16.647 +	  let val (env',flexflex,flexrigid) = 
  16.648 +	       (if tdepth> !trace_bound andalso !trace_simp
  16.649 +		then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
  16.650 +		SIMPL (env,dpairs))
  16.651 +	  in case flexrigid of
  16.652 +	      [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
  16.653 +	    | dp::frigid' => 
  16.654 +		if tdepth > !search_bound then
  16.655 +		    (prs"***Unification bound exceeded\n"; Sequence.pull reseq)
  16.656 +		else
  16.657 +		(if tdepth > !trace_bound then
  16.658 +		    print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
  16.659 +		 else ();
  16.660 +		 Sequence.pull (Sequence.its_right (add_unify (tdepth+1))
  16.661 +			   (MATCH (env',dp, frigid'@flexflex), reseq)))
  16.662 +	  end
  16.663 +	  handle CANTUNIFY => 
  16.664 +	    (if tdepth > !trace_bound then writeln"Failure node" else ();
  16.665 +	     Sequence.pull reseq));
  16.666       val dps = map (fn(t,u)=> ([],t,u)) tus
  16.667    in sgr := sg;
  16.668       add_unify 1 ((env,dps), Sequence.null) 
  16.669 @@ -675,7 +675,7 @@
  16.670  (*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
  16.671    Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
  16.672    Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a, 
  16.673 -        though just ?g->?f is a more general unifier.
  16.674 +	though just ?g->?f is a more general unifier.
  16.675    Unlike Huet (1975), does not smash together all variables of same type --
  16.676      requires more work yet gives a less general unifier (fewer variables).
  16.677    Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)