fixed warning;
authorwenzelm
Fri Dec 13 17:38:17 1996 +0100 (1996-12-13)
changeset 238658f8ff014009
parent 2385 73d1435aa729
child 2387 1b37895b607a
fixed warning;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Fri Dec 13 17:37:42 1996 +0100
     1.2 +++ b/src/Pure/thm.ML	Fri Dec 13 17:38:17 1996 +0100
     1.3 @@ -39,40 +39,40 @@
     1.4  
     1.5    (*proof terms [must duplicate declaration as a specification]*)
     1.6    datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
     1.7 -  val keep_derivs	: deriv_kind ref
     1.8 +  val keep_derivs       : deriv_kind ref
     1.9    datatype rule = 
    1.10 -      MinProof				
    1.11 +      MinProof                          
    1.12      | Oracle of theory * Sign.sg * exn
    1.13 -    | Axiom		of theory * string
    1.14 -    | Theorem		of string	
    1.15 -    | Assume		of cterm
    1.16 -    | Implies_intr	of cterm
    1.17 +    | Axiom             of theory * string
    1.18 +    | Theorem           of string       
    1.19 +    | Assume            of cterm
    1.20 +    | Implies_intr      of cterm
    1.21      | Implies_intr_shyps
    1.22      | Implies_intr_hyps
    1.23      | Implies_elim 
    1.24 -    | Forall_intr	of cterm
    1.25 -    | Forall_elim	of cterm
    1.26 -    | Reflexive		of cterm
    1.27 +    | Forall_intr       of cterm
    1.28 +    | Forall_elim       of cterm
    1.29 +    | Reflexive         of cterm
    1.30      | Symmetric 
    1.31      | Transitive
    1.32 -    | Beta_conversion	of cterm
    1.33 +    | Beta_conversion   of cterm
    1.34      | Extensional
    1.35 -    | Abstract_rule	of string * cterm
    1.36 +    | Abstract_rule     of string * cterm
    1.37      | Combination
    1.38      | Equal_intr
    1.39      | Equal_elim
    1.40 -    | Trivial		of cterm
    1.41 -    | Lift_rule		of cterm * int 
    1.42 -    | Assumption	of int * Envir.env option
    1.43 -    | Instantiate	of (indexname * ctyp) list * (cterm * cterm) list
    1.44 -    | Bicompose		of bool * bool * int * int * Envir.env
    1.45 -    | Flexflex_rule	of Envir.env		
    1.46 -    | Class_triv	of theory * class	
    1.47 +    | Trivial           of cterm
    1.48 +    | Lift_rule         of cterm * int 
    1.49 +    | Assumption        of int * Envir.env option
    1.50 +    | Instantiate       of (indexname * ctyp) list * (cterm * cterm) list
    1.51 +    | Bicompose         of bool * bool * int * int * Envir.env
    1.52 +    | Flexflex_rule     of Envir.env            
    1.53 +    | Class_triv        of theory * class       
    1.54      | VarifyT
    1.55      | FreezeT
    1.56 -    | RewriteC		of cterm
    1.57 -    | CongC		of cterm
    1.58 -    | Rewrite_cterm	of cterm
    1.59 +    | RewriteC          of cterm
    1.60 +    | CongC             of cterm
    1.61 +    | Rewrite_cterm     of cterm
    1.62      | Rename_params_rule of string list * int;
    1.63  
    1.64    type deriv   (* = rule mtree *)
    1.65 @@ -81,11 +81,11 @@
    1.66    type thm
    1.67    exception THM of string * int * thm list
    1.68    val rep_thm           : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
    1.69 -				  shyps: sort list, hyps: term list, 
    1.70 -				  prop: term}
    1.71 +                                  shyps: sort list, hyps: term list, 
    1.72 +                                  prop: term}
    1.73    val crep_thm          : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
    1.74 -				  shyps: sort list, hyps: cterm list, 
    1.75 -				  prop: cterm}
    1.76 +                                  shyps: sort list, hyps: cterm list, 
    1.77 +                                  prop: cterm}
    1.78    val stamps_of_thm     : thm -> string ref list
    1.79    val tpairs_of         : thm -> (term * term) list
    1.80    val prems_of          : thm -> term list
    1.81 @@ -152,7 +152,7 @@
    1.82    val rewrite_cterm     : bool * bool -> meta_simpset ->
    1.83                            (meta_simpset -> thm -> thm option) -> cterm -> thm
    1.84  
    1.85 -  val invoke_oracle	: theory * Sign.sg * exn -> thm
    1.86 +  val invoke_oracle     : theory * Sign.sg * exn -> thm
    1.87  end;
    1.88  
    1.89  structure Thm : THM =
    1.90 @@ -248,7 +248,7 @@
    1.91            Sign.infer_types sign types sorts used freeze (ts, T');
    1.92      val ct = cterm_of sign t'
    1.93        handle TYPE arg => error (Sign.exn_type_msg sign arg)
    1.94 -	   | TERM (msg, _) => error msg;
    1.95 +           | TERM (msg, _) => error msg;
    1.96    in (ct, tye) end;
    1.97  
    1.98  fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true;
    1.99 @@ -260,14 +260,14 @@
   1.100    let
   1.101      val {tsig, syn, ...} = Sign.rep_sg sign
   1.102      fun read (b,T) =
   1.103 -	case Syntax.read syn T b of
   1.104 -	    [t] => t
   1.105 -	  | _   => error("Error or ambiguity in parsing of " ^ b)
   1.106 +        case Syntax.read syn T b of
   1.107 +            [t] => t
   1.108 +          | _   => error("Error or ambiguity in parsing of " ^ b)
   1.109      val (us,_) = Type.infer_types(tsig, Sign.const_type sign, 
   1.110 -				  K None, K None, 
   1.111 -				  [], true, 
   1.112 -				  map (Sign.certify_typ sign) Ts, 
   1.113 -				  ListPair.map read (bs,Ts))
   1.114 +                                  K None, K None, 
   1.115 +                                  [], true, 
   1.116 +                                  map (Sign.certify_typ sign) Ts, 
   1.117 +                                  ListPair.map read (bs,Ts))
   1.118    in  map (cterm_of sign) us  end
   1.119    handle TYPE arg => error (Sign.exn_type_msg sign arg)
   1.120         | TERM (msg, _) => error msg;
   1.121 @@ -279,47 +279,47 @@
   1.122  (*Names of rules in derivations.  Includes logically trivial rules, if 
   1.123    executed in ML.*)
   1.124  datatype rule = 
   1.125 -    MinProof				(*for building minimal proof terms*)
   1.126 -  | Oracle   	        of theory * Sign.sg * exn	(*oracles*)
   1.127 +    MinProof                            (*for building minimal proof terms*)
   1.128 +  | Oracle              of theory * Sign.sg * exn       (*oracles*)
   1.129  (*Axioms/theorems*)
   1.130 -  | Axiom		of theory * string
   1.131 -  | Theorem		of string
   1.132 +  | Axiom               of theory * string
   1.133 +  | Theorem             of string
   1.134  (*primitive inferences and compound versions of them*)
   1.135 -  | Assume		of cterm
   1.136 -  | Implies_intr	of cterm
   1.137 +  | Assume              of cterm
   1.138 +  | Implies_intr        of cterm
   1.139    | Implies_intr_shyps
   1.140    | Implies_intr_hyps
   1.141    | Implies_elim 
   1.142 -  | Forall_intr		of cterm
   1.143 -  | Forall_elim		of cterm
   1.144 -  | Reflexive		of cterm
   1.145 +  | Forall_intr         of cterm
   1.146 +  | Forall_elim         of cterm
   1.147 +  | Reflexive           of cterm
   1.148    | Symmetric 
   1.149    | Transitive
   1.150 -  | Beta_conversion	of cterm
   1.151 +  | Beta_conversion     of cterm
   1.152    | Extensional
   1.153 -  | Abstract_rule	of string * cterm
   1.154 +  | Abstract_rule       of string * cterm
   1.155    | Combination
   1.156    | Equal_intr
   1.157    | Equal_elim
   1.158  (*derived rules for tactical proof*)
   1.159 -  | Trivial		of cterm
   1.160 -	(*For lift_rule, the proof state is not a premise.
   1.161 -	  Use cterm instead of thm to avoid mutual recursion.*)
   1.162 -  | Lift_rule		of cterm * int 
   1.163 -  | Assumption		of int * Envir.env option (*includes eq_assumption*)
   1.164 -  | Instantiate		of (indexname * ctyp) list * (cterm * cterm) list
   1.165 -  | Bicompose		of bool * bool * int * int * Envir.env
   1.166 -  | Flexflex_rule	of Envir.env		(*identifies unifier chosen*)
   1.167 +  | Trivial             of cterm
   1.168 +        (*For lift_rule, the proof state is not a premise.
   1.169 +          Use cterm instead of thm to avoid mutual recursion.*)
   1.170 +  | Lift_rule           of cterm * int 
   1.171 +  | Assumption          of int * Envir.env option (*includes eq_assumption*)
   1.172 +  | Instantiate         of (indexname * ctyp) list * (cterm * cterm) list
   1.173 +  | Bicompose           of bool * bool * int * int * Envir.env
   1.174 +  | Flexflex_rule       of Envir.env            (*identifies unifier chosen*)
   1.175  (*other derived rules*)
   1.176 -  | Class_triv		of theory * class	(*derived rule????*)
   1.177 +  | Class_triv          of theory * class       (*derived rule????*)
   1.178    | VarifyT
   1.179    | FreezeT
   1.180  (*for the simplifier*)
   1.181 -  | RewriteC		of cterm
   1.182 -  | CongC		of cterm
   1.183 -  | Rewrite_cterm	of cterm
   1.184 +  | RewriteC            of cterm
   1.185 +  | CongC               of cterm
   1.186 +  | Rewrite_cterm       of cterm
   1.187  (*Logical identities, recorded since they are part of the proof process*)
   1.188 -  | Rename_params_rule	of string list * int;
   1.189 +  | Rename_params_rule  of string list * int;
   1.190  
   1.191  
   1.192  type deriv = rule mtree;
   1.193 @@ -334,15 +334,15 @@
   1.194  fun squash_derivs [] = []
   1.195    | squash_derivs (der::ders) =
   1.196       (case der of
   1.197 -	  Join (Oracle _, _) => der :: squash_derivs ders
   1.198 -	| Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 
   1.199 -				      then der :: squash_derivs ders
   1.200 -				      else squash_derivs (der'::ders)
   1.201 -	| Join (Axiom _, _) => if !keep_derivs=ThmDeriv 
   1.202 -			       then der :: squash_derivs ders
   1.203 -			       else squash_derivs ders
   1.204 -	| Join (_, [])      => squash_derivs ders
   1.205 -	| _                 => der :: squash_derivs ders);
   1.206 +          Join (Oracle _, _) => der :: squash_derivs ders
   1.207 +        | Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 
   1.208 +                                      then der :: squash_derivs ders
   1.209 +                                      else squash_derivs (der'::ders)
   1.210 +        | Join (Axiom _, _) => if !keep_derivs=ThmDeriv 
   1.211 +                               then der :: squash_derivs ders
   1.212 +                               else squash_derivs ders
   1.213 +        | Join (_, [])      => squash_derivs ders
   1.214 +        | _                 => der :: squash_derivs ders);
   1.215  
   1.216  
   1.217  (*Ensure sharing of the most likely derivation, the empty one!*)
   1.218 @@ -362,12 +362,12 @@
   1.219  (*** Meta theorems ***)
   1.220  
   1.221  datatype thm = Thm of
   1.222 -  {sign: Sign.sg,		(*signature for hyps and prop*)
   1.223 -   der: deriv,			(*derivation*)
   1.224 -   maxidx: int,			(*maximum index of any Var or TVar*)
   1.225 -   shyps: sort list,		(*sort hypotheses*)
   1.226 -   hyps: term list,		(*hypotheses*)
   1.227 -   prop: term};			(*conclusion*)
   1.228 +  {sign: Sign.sg,               (*signature for hyps and prop*)
   1.229 +   der: deriv,                  (*derivation*)
   1.230 +   maxidx: int,                 (*maximum index of any Var or TVar*)
   1.231 +   shyps: sort list,            (*sort hypotheses*)
   1.232 +   hyps: term list,             (*hypotheses*)
   1.233 +   prop: term};                 (*conclusion*)
   1.234  
   1.235  fun rep_thm (Thm args) = args;
   1.236  
   1.237 @@ -463,9 +463,9 @@
   1.238        add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, [])));
   1.239    in
   1.240      Thm {sign = sign, 
   1.241 -	 der = der,		(*No new derivation, as other rules call this*)
   1.242 -	 maxidx = maxidx,
   1.243 -	 shyps = shyps, hyps = hyps, prop = prop}
   1.244 +         der = der,             (*No new derivation, as other rules call this*)
   1.245 +         maxidx = maxidx,
   1.246 +         shyps = shyps, hyps = hyps, prop = prop}
   1.247    end;
   1.248  
   1.249  
   1.250 @@ -482,13 +482,13 @@
   1.251      val shyps' = filter (fn S => mem_sort(S,sorts) orelse maybe_empty S) shyps;
   1.252    in
   1.253      Thm {sign = sign, der = der, maxidx = maxidx,
   1.254 -	 shyps =
   1.255 -	 (if eq_set_sort (shyps',sorts) orelse 
   1.256 -	     not (!force_strip_shyps) then shyps'
   1.257 -	  else    (* FIXME tmp *)
   1.258 -	      (writeln ("WARNING Removed sort hypotheses: " ^
   1.259 -			commas (map Type.str_of_sort (shyps' \\ sorts)));
   1.260 -	       writeln "WARNING Let's hope these sorts are non-empty!";
   1.261 +         shyps =
   1.262 +         (if eq_set_sort (shyps',sorts) orelse 
   1.263 +             not (!force_strip_shyps) then shyps'
   1.264 +          else    (* FIXME tmp *)
   1.265 +              (warning ("Removed sort hypotheses: " ^
   1.266 +                        commas (map Type.str_of_sort (shyps' \\ sorts)));
   1.267 +               warning "Let's hope these sorts are non-empty!";
   1.268             sorts)),
   1.269        hyps = hyps, 
   1.270        prop = prop}
   1.271 @@ -514,11 +514,11 @@
   1.272          val sort_hyps = flat (map2 mk_insort (tfrees, xshyps));
   1.273        in
   1.274          Thm {sign = sign, 
   1.275 -	     der = infer_derivs (Implies_intr_shyps, [der]), 
   1.276 -	     maxidx = maxidx, 
   1.277 -	     shyps = shyps',
   1.278 -	     hyps = hyps, 
   1.279 -	     prop = Logic.list_implies (sort_hyps, prop)}
   1.280 +             der = infer_derivs (Implies_intr_shyps, [der]), 
   1.281 +             maxidx = maxidx, 
   1.282 +             shyps = shyps',
   1.283 +             hyps = hyps, 
   1.284 +             prop = Logic.list_implies (sort_hyps, prop)}
   1.285        end);
   1.286  
   1.287  
   1.288 @@ -529,16 +529,16 @@
   1.289    let
   1.290      fun get_ax [] = raise Match
   1.291        | get_ax (thy :: thys) =
   1.292 -	  let val {sign, new_axioms, parents, ...} = rep_theory thy
   1.293 +          let val {sign, new_axioms, parents, ...} = rep_theory thy
   1.294            in case Symtab.lookup (new_axioms, name) of
   1.295 -		Some t => fix_shyps [] []
   1.296 -		           (Thm {sign = sign, 
   1.297 -				 der = infer_derivs (Axiom(theory,name), []),
   1.298 -				 maxidx = maxidx_of_term t,
   1.299 -				 shyps = [], 
   1.300 -				 hyps = [], 
   1.301 -				 prop = t})
   1.302 -	      | None => get_ax parents handle Match => get_ax thys
   1.303 +                Some t => fix_shyps [] []
   1.304 +                           (Thm {sign = sign, 
   1.305 +                                 der = infer_derivs (Axiom(theory,name), []),
   1.306 +                                 maxidx = maxidx_of_term t,
   1.307 +                                 shyps = [], 
   1.308 +                                 hyps = [], 
   1.309 +                                 prop = t})
   1.310 +              | None => get_ax parents handle Match => get_ax thys
   1.311            end;
   1.312    in
   1.313      get_ax [theory] handle Match
   1.314 @@ -554,22 +554,22 @@
   1.315  (*Attach a label to a theorem to make proof objects more readable*)
   1.316  fun name_thm (name, th as Thm {sign, der, maxidx, shyps, hyps, prop}) = 
   1.317      Thm {sign = sign, 
   1.318 -	 der = Join (Theorem name, [der]),
   1.319 -	 maxidx = maxidx,
   1.320 -	 shyps = shyps, 
   1.321 -	 hyps = hyps, 
   1.322 -	 prop = prop};
   1.323 +         der = Join (Theorem name, [der]),
   1.324 +         maxidx = maxidx,
   1.325 +         shyps = shyps, 
   1.326 +         hyps = hyps, 
   1.327 +         prop = prop};
   1.328  
   1.329  
   1.330  (*Compression of theorems -- a separate rule, not integrated with the others,
   1.331    as it could be slow.*)
   1.332  fun compress (Thm {sign, der, maxidx, shyps, hyps, prop}) = 
   1.333      Thm {sign = sign, 
   1.334 -	 der = der,	(*No derivation recorded!*)
   1.335 -	 maxidx = maxidx,
   1.336 -	 shyps = shyps, 
   1.337 -	 hyps = map Term.compress_term hyps, 
   1.338 -	 prop = Term.compress_term prop};
   1.339 +         der = der,     (*No derivation recorded!*)
   1.340 +         maxidx = maxidx,
   1.341 +         shyps = shyps, 
   1.342 +         hyps = map Term.compress_term hyps, 
   1.343 +         prop = Term.compress_term prop};
   1.344  
   1.345  
   1.346  (*** Meta rules ***)
   1.347 @@ -580,11 +580,11 @@
   1.348  fun nodup_Vars (thm as Thm{sign, der, maxidx, shyps, hyps, prop}) s =
   1.349    (Sign.nodup_Vars prop; 
   1.350     Thm {sign = sign, 
   1.351 -	 der = der,	
   1.352 -	 maxidx = maxidx_of_term prop,
   1.353 -	 shyps = shyps, 
   1.354 -	 hyps = hyps, 
   1.355 -	 prop = prop})
   1.356 +         der = der,     
   1.357 +         maxidx = maxidx_of_term prop,
   1.358 +         shyps = shyps, 
   1.359 +         hyps = hyps, 
   1.360 +         prop = prop})
   1.361    handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts);
   1.362  
   1.363  (** 'primitive' rules **)
   1.364 @@ -601,11 +601,11 @@
   1.365          raise THM("assume: assumptions may not contain scheme variables",
   1.366                    maxidx, [])
   1.367        else Thm{sign   = sign, 
   1.368 -	       der    = infer_derivs (Assume ct, []), 
   1.369 -	       maxidx = ~1, 
   1.370 -	       shyps  = add_term_sorts(prop,[]), 
   1.371 -	       hyps   = [prop], 
   1.372 -	       prop   = prop}
   1.373 +               der    = infer_derivs (Assume ct, []), 
   1.374 +               maxidx = ~1, 
   1.375 +               shyps  = add_term_sorts(prop,[]), 
   1.376 +               hyps   = [prop], 
   1.377 +               prop   = prop}
   1.378    end;
   1.379  
   1.380  (*Implication introduction
   1.381 @@ -619,11 +619,11 @@
   1.382          raise THM("implies_intr: assumptions must have type prop", 0, [thB])
   1.383        else fix_shyps [thB] []
   1.384          (Thm{sign = Sign.merge (sign,signA),  
   1.385 -	     der = infer_derivs (Implies_intr cA, [der]),
   1.386 -	     maxidx = Int.max(maxidxA, maxidx),
   1.387 -	     shyps = [],
   1.388 -	     hyps = disch(hyps,A),
   1.389 -	     prop = implies$A$prop})
   1.390 +             der = infer_derivs (Implies_intr cA, [der]),
   1.391 +             maxidx = Int.max(maxidxA, maxidx),
   1.392 +             shyps = [],
   1.393 +             hyps = disch(hyps,A),
   1.394 +             prop = implies$A$prop})
   1.395        handle TERM _ =>
   1.396          raise THM("implies_intr: incompatible signatures", 0, [thB])
   1.397    end;
   1.398 @@ -643,11 +643,11 @@
   1.399                  if imp=implies andalso  A aconv propA
   1.400                  then fix_shyps [thAB, thA] []
   1.401                         (Thm{sign= merge_thm_sgs(thAB,thA),
   1.402 -			    der = infer_derivs (Implies_elim, [der,derA]),
   1.403 -			    maxidx = Int.max(maxA,maxidx),
   1.404 -			    shyps = [],
   1.405 -			    hyps = union_term(hypsA,hyps),  (*dups suppressed*)
   1.406 -			    prop = B})
   1.407 +                            der = infer_derivs (Implies_elim, [der,derA]),
   1.408 +                            maxidx = Int.max(maxA,maxidx),
   1.409 +                            shyps = [],
   1.410 +                            hyps = union_term(hypsA,hyps),  (*dups suppressed*)
   1.411 +                            prop = B})
   1.412                  else err("major premise")
   1.413            | _ => err("major premise")
   1.414      end;
   1.415 @@ -661,11 +661,11 @@
   1.416    let val x = term_of cx;
   1.417        fun result(a,T) = fix_shyps [th] []
   1.418          (Thm{sign = sign, 
   1.419 -	     der = infer_derivs (Forall_intr cx, [der]),
   1.420 -	     maxidx = maxidx,
   1.421 -	     shyps = [],
   1.422 -	     hyps = hyps,
   1.423 -	     prop = all(T) $ Abs(a, T, abstract_over (x,prop))})
   1.424 +             der = infer_derivs (Forall_intr cx, [der]),
   1.425 +             maxidx = maxidx,
   1.426 +             shyps = [],
   1.427 +             hyps = hyps,
   1.428 +             prop = all(T) $ Abs(a, T, abstract_over (x,prop))})
   1.429    in  case x of
   1.430          Free(a,T) =>
   1.431            if exists (apl(x, Logic.occs)) hyps
   1.432 @@ -683,20 +683,20 @@
   1.433  fun forall_elim ct (th as Thm{sign,der,maxidx,hyps,prop,...}) : thm =
   1.434    let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct
   1.435    in  case prop of
   1.436 -	Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
   1.437 -	  if T<>qary then
   1.438 -	      raise THM("forall_elim: type mismatch", 0, [th])
   1.439 -	  else let val thm = fix_shyps [th] []
   1.440 -		    (Thm{sign= Sign.merge(sign,signt),
   1.441 -			 der = infer_derivs (Forall_elim ct, [der]),
   1.442 -			 maxidx = Int.max(maxidx, maxt),
   1.443 -			 shyps = [],
   1.444 -			 hyps = hyps,  
   1.445 -			 prop = betapply(A,t)})
   1.446 -	       in if maxt >= 0 andalso maxidx >= 0
   1.447 -		  then nodup_Vars thm "forall_elim" 
   1.448 -		  else thm (*no new Vars: no expensive check!*)
   1.449 -	       end
   1.450 +        Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
   1.451 +          if T<>qary then
   1.452 +              raise THM("forall_elim: type mismatch", 0, [th])
   1.453 +          else let val thm = fix_shyps [th] []
   1.454 +                    (Thm{sign= Sign.merge(sign,signt),
   1.455 +                         der = infer_derivs (Forall_elim ct, [der]),
   1.456 +                         maxidx = Int.max(maxidx, maxt),
   1.457 +                         shyps = [],
   1.458 +                         hyps = hyps,  
   1.459 +                         prop = betapply(A,t)})
   1.460 +               in if maxt >= 0 andalso maxidx >= 0
   1.461 +                  then nodup_Vars thm "forall_elim" 
   1.462 +                  else thm (*no new Vars: no expensive check!*)
   1.463 +               end
   1.464        | _ => raise THM("forall_elim: not quantified", 0, [th])
   1.465    end
   1.466    handle TERM _ =>
   1.467 @@ -713,18 +713,18 @@
   1.468         hyps = [], 
   1.469         maxidx = 0,
   1.470         prop = term_of (read_cterm Sign.proto_pure
   1.471 -		       ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))});
   1.472 +                       ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))});
   1.473  
   1.474  (*The reflexivity rule: maps  t   to the theorem   t==t   *)
   1.475  fun reflexive ct =
   1.476    let val {sign, t, T, maxidx} = rep_cterm ct
   1.477    in  fix_shyps [] []
   1.478         (Thm{sign= sign, 
   1.479 -	    der = infer_derivs (Reflexive ct, []),
   1.480 -	    shyps = [],
   1.481 -	    hyps = [], 
   1.482 -	    maxidx = maxidx,
   1.483 -	    prop = Logic.mk_equals(t,t)})
   1.484 +            der = infer_derivs (Reflexive ct, []),
   1.485 +            shyps = [],
   1.486 +            hyps = [], 
   1.487 +            maxidx = maxidx,
   1.488 +            prop = Logic.mk_equals(t,t)})
   1.489    end;
   1.490  
   1.491  (*The symmetry rule
   1.492 @@ -736,12 +736,12 @@
   1.493    case prop of
   1.494        (eq as Const("==",_)) $ t $ u =>
   1.495          (*no fix_shyps*)
   1.496 -	  Thm{sign = sign,
   1.497 -	      der = infer_derivs (Symmetric, [der]),
   1.498 -	      maxidx = maxidx,
   1.499 -	      shyps = shyps,
   1.500 -	      hyps = hyps,
   1.501 -	      prop = eq$u$t}
   1.502 +          Thm{sign = sign,
   1.503 +              der = infer_derivs (Symmetric, [der]),
   1.504 +              maxidx = maxidx,
   1.505 +              shyps = shyps,
   1.506 +              hyps = hyps,
   1.507 +              prop = eq$u$t}
   1.508      | _ => raise THM("symmetric", 0, [th]);
   1.509  
   1.510  (*The transitive rule
   1.511 @@ -759,11 +759,11 @@
   1.512            else let val thm =      
   1.513                fix_shyps [th1, th2] []
   1.514                  (Thm{sign= merge_thm_sgs(th1,th2), 
   1.515 -		     der = infer_derivs (Transitive, [der1, der2]),
   1.516 +                     der = infer_derivs (Transitive, [der1, der2]),
   1.517                       maxidx = Int.max(max1,max2), 
   1.518 -		     shyps = [],
   1.519 -		     hyps = union_term(hyps1,hyps2),
   1.520 -		     prop = eq$t1$t2})
   1.521 +                     shyps = [],
   1.522 +                     hyps = union_term(hyps1,hyps2),
   1.523 +                     prop = eq$t1$t2})
   1.524                   in if max1 >= 0 andalso max2 >= 0
   1.525                      then nodup_Vars thm "transitive" 
   1.526                      else thm (*no new Vars: no expensive check!*)
   1.527 @@ -777,11 +777,11 @@
   1.528    in  case t of
   1.529            Abs(_,_,bodt) $ u => fix_shyps [] []
   1.530              (Thm{sign = sign,  
   1.531 -		 der = infer_derivs (Beta_conversion ct, []),
   1.532 -		 maxidx = maxidx,
   1.533 -		 shyps = [],
   1.534 -		 hyps = [],
   1.535 -		 prop = Logic.mk_equals(t, subst_bound (u,bodt))})
   1.536 +                 der = infer_derivs (Beta_conversion ct, []),
   1.537 +                 maxidx = maxidx,
   1.538 +                 shyps = [],
   1.539 +                 hyps = [],
   1.540 +                 prop = Logic.mk_equals(t, subst_bound (u,bodt))})
   1.541          | _ =>  raise THM("beta_conversion: not a redex", 0, [])
   1.542    end;
   1.543  
   1.544 @@ -805,10 +805,10 @@
   1.545                | _ => err"not a variable");
   1.546            (*no fix_shyps*)
   1.547            Thm{sign = sign,
   1.548 -	      der = infer_derivs (Extensional, [der]),
   1.549 -	      maxidx = maxidx,
   1.550 -	      shyps = shyps,
   1.551 -	      hyps = hyps, 
   1.552 +              der = infer_derivs (Extensional, [der]),
   1.553 +              maxidx = maxidx,
   1.554 +              shyps = shyps,
   1.555 +              hyps = hyps, 
   1.556                prop = Logic.mk_equals(f,g)}
   1.557        end
   1.558   | _ =>  raise THM("extensional: premise", 0, [th]);
   1.559 @@ -825,13 +825,13 @@
   1.560              handle TERM _ =>
   1.561                  raise THM("abstract_rule: premise not an equality", 0, [th])
   1.562        fun result T = fix_shyps [th] []
   1.563 -	  (Thm{sign = sign,
   1.564 -	       der = infer_derivs (Abstract_rule (a,cx), [der]),
   1.565 -	       maxidx = maxidx, 
   1.566 -	       shyps = [], 
   1.567 -	       hyps = hyps,
   1.568 -	       prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)),
   1.569 -				      Abs(a, T, abstract_over (x,u)))})
   1.570 +          (Thm{sign = sign,
   1.571 +               der = infer_derivs (Abstract_rule (a,cx), [der]),
   1.572 +               maxidx = maxidx, 
   1.573 +               shyps = [], 
   1.574 +               hyps = hyps,
   1.575 +               prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)),
   1.576 +                                      Abs(a, T, abstract_over (x,u)))})
   1.577    in  case x of
   1.578          Free(_,T) =>
   1.579           if exists (apl(x, Logic.occs)) hyps
   1.580 @@ -848,30 +848,30 @@
   1.581  *)
   1.582  fun combination th1 th2 =
   1.583    let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
   1.584 -	      prop=prop1,...} = th1
   1.585 +              prop=prop1,...} = th1
   1.586        and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
   1.587 -	      prop=prop2,...} = th2
   1.588 +              prop=prop2,...} = th2
   1.589        fun chktypes (f,t) =
   1.590 -	    (case fastype_of f of
   1.591 -		Type("fun",[T1,T2]) => 
   1.592 -		    if T1 <> fastype_of t then
   1.593 -			 raise THM("combination: types", 0, [th1,th2])
   1.594 -		    else ()
   1.595 -		| _ => raise THM("combination: not function type", 0, 
   1.596 -				 [th1,th2]))
   1.597 +            (case fastype_of f of
   1.598 +                Type("fun",[T1,T2]) => 
   1.599 +                    if T1 <> fastype_of t then
   1.600 +                         raise THM("combination: types", 0, [th1,th2])
   1.601 +                    else ()
   1.602 +                | _ => raise THM("combination: not function type", 0, 
   1.603 +                                 [th1,th2]))
   1.604    in case (prop1,prop2)  of
   1.605         (Const("==",_) $ f $ g, Const("==",_) $ t $ u) =>
   1.606            let val _   = chktypes (f,t)
   1.607 -	      val thm = (*no fix_shyps*)
   1.608 -			Thm{sign = merge_thm_sgs(th1,th2), 
   1.609 -			    der = infer_derivs (Combination, [der1, der2]),
   1.610 -			    maxidx = Int.max(max1,max2), 
   1.611 -			    shyps = union_sort(shyps1,shyps2),
   1.612 -			    hyps = union_term(hyps1,hyps2),
   1.613 -			    prop = Logic.mk_equals(f$t, g$u)}
   1.614 +              val thm = (*no fix_shyps*)
   1.615 +                        Thm{sign = merge_thm_sgs(th1,th2), 
   1.616 +                            der = infer_derivs (Combination, [der1, der2]),
   1.617 +                            maxidx = Int.max(max1,max2), 
   1.618 +                            shyps = union_sort(shyps1,shyps2),
   1.619 +                            hyps = union_term(hyps1,hyps2),
   1.620 +                            prop = Logic.mk_equals(f$t, g$u)}
   1.621            in if max1 >= 0 andalso max2 >= 0
   1.622               then nodup_Vars thm "combination" 
   1.623 -	     else thm (*no new Vars: no expensive check!*)  
   1.624 +             else thm (*no new Vars: no expensive check!*)  
   1.625            end
   1.626       | _ =>  raise THM("combination: premises", 0, [th1,th2])
   1.627    end;
   1.628 @@ -884,22 +884,22 @@
   1.629  *)
   1.630  fun equal_intr th1 th2 =
   1.631    let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1, 
   1.632 -	      prop=prop1,...} = th1
   1.633 +              prop=prop1,...} = th1
   1.634        and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
   1.635 -	      prop=prop2,...} = th2;
   1.636 +              prop=prop2,...} = th2;
   1.637        fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2])
   1.638    in case (prop1,prop2) of
   1.639         (Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A')  =>
   1.640 -	  if A aconv A' andalso B aconv B'
   1.641 -	  then
   1.642 -	    (*no fix_shyps*)
   1.643 -	      Thm{sign = merge_thm_sgs(th1,th2),
   1.644 -		  der = infer_derivs (Equal_intr, [der1, der2]),
   1.645 -		  maxidx = Int.max(max1,max2),
   1.646 -		  shyps = union_sort(shyps1,shyps2),
   1.647 -		  hyps = union_term(hyps1,hyps2),
   1.648 -		  prop = Logic.mk_equals(A,B)}
   1.649 -	  else err"not equal"
   1.650 +          if A aconv A' andalso B aconv B'
   1.651 +          then
   1.652 +            (*no fix_shyps*)
   1.653 +              Thm{sign = merge_thm_sgs(th1,th2),
   1.654 +                  der = infer_derivs (Equal_intr, [der1, der2]),
   1.655 +                  maxidx = Int.max(max1,max2),
   1.656 +                  shyps = union_sort(shyps1,shyps2),
   1.657 +                  hyps = union_term(hyps1,hyps2),
   1.658 +                  prop = Logic.mk_equals(A,B)}
   1.659 +          else err"not equal"
   1.660       | _ =>  err"premises"
   1.661    end;
   1.662  
   1.663 @@ -918,11 +918,11 @@
   1.664            if not (prop2 aconv A) then err"not equal"  else
   1.665              fix_shyps [th1, th2] []
   1.666                (Thm{sign= merge_thm_sgs(th1,th2), 
   1.667 -		   der = infer_derivs (Equal_elim, [der1, der2]),
   1.668 -		   maxidx = Int.max(max1,max2),
   1.669 -		   shyps = [],
   1.670 -		   hyps = union_term(hyps1,hyps2),
   1.671 -		   prop = B})
   1.672 +                   der = infer_derivs (Equal_elim, [der1, der2]),
   1.673 +                   maxidx = Int.max(max1,max2),
   1.674 +                   shyps = [],
   1.675 +                   hyps = union_term(hyps1,hyps2),
   1.676 +                   prop = B})
   1.677       | _ =>  err"major premise"
   1.678    end;
   1.679  
   1.680 @@ -935,11 +935,11 @@
   1.681  fun implies_intr_hyps (Thm{sign, der, maxidx, shyps, hyps=A::As, prop}) =
   1.682        implies_intr_hyps (*no fix_shyps*)
   1.683              (Thm{sign = sign, 
   1.684 -		 der = infer_derivs (Implies_intr_hyps, [der]), 
   1.685 -		 maxidx = maxidx, 
   1.686 -		 shyps = shyps,
   1.687 +                 der = infer_derivs (Implies_intr_hyps, [der]), 
   1.688 +                 maxidx = maxidx, 
   1.689 +                 shyps = shyps,
   1.690                   hyps = disch(As,A),  
   1.691 -		 prop = implies$A$prop})
   1.692 +                 prop = implies$A$prop})
   1.693    | implies_intr_hyps th = th;
   1.694  
   1.695  (*Smash" unifies the list of term pairs leaving no flex-flex pairs.
   1.696 @@ -957,11 +957,11 @@
   1.697                val newprop = Logic.list_flexpairs(distpairs, horn)
   1.698            in  fix_shyps [th] (env_codT env)
   1.699                  (Thm{sign = sign, 
   1.700 -		     der = infer_derivs (Flexflex_rule env, [der]), 
   1.701 -		     maxidx = maxidx_of_term newprop, 
   1.702 -		     shyps = [], 
   1.703 -		     hyps = hyps,
   1.704 -		     prop = newprop})
   1.705 +                     der = infer_derivs (Flexflex_rule env, [der]), 
   1.706 +                     maxidx = maxidx_of_term newprop, 
   1.707 +                     shyps = [], 
   1.708 +                     hyps = hyps,
   1.709 +                     prop = newprop})
   1.710            end;
   1.711        val (tpairs,_) = Logic.strip_flexpairs prop
   1.712    in Sequence.maps newthm
   1.713 @@ -1003,11 +1003,11 @@
   1.714        val newth =
   1.715              fix_shyps [th] (map snd vTs)
   1.716                (Thm{sign = newsign, 
   1.717 -		   der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 
   1.718 -		   maxidx = maxidx_of_term newprop, 
   1.719 -		   shyps = [],
   1.720 -		   hyps = hyps,
   1.721 -		   prop = newprop})
   1.722 +                   der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 
   1.723 +                   maxidx = maxidx_of_term newprop, 
   1.724 +                   shyps = [],
   1.725 +                   hyps = hyps,
   1.726 +                   prop = newprop})
   1.727    in  if not(instl_ok(map #1 tpairs))
   1.728        then raise THM("instantiate: variables not distinct", 0, [th])
   1.729        else if not(null(findrep(map #1 vTs)))
   1.730 @@ -1026,27 +1026,27 @@
   1.731              raise THM("trivial: the term must have type prop", 0, [])
   1.732        else fix_shyps [] []
   1.733          (Thm{sign = sign, 
   1.734 -	     der = infer_derivs (Trivial ct, []), 
   1.735 -	     maxidx = maxidx, 
   1.736 -	     shyps = [], 
   1.737 -	     hyps = [],
   1.738 -	     prop = implies$A$A})
   1.739 +             der = infer_derivs (Trivial ct, []), 
   1.740 +             maxidx = maxidx, 
   1.741 +             shyps = [], 
   1.742 +             hyps = [],
   1.743 +             prop = implies$A$A})
   1.744    end;
   1.745  
   1.746  (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
   1.747  fun class_triv thy c =
   1.748    let val sign = sign_of thy;
   1.749        val Cterm {t, maxidx, ...} =
   1.750 -	  cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
   1.751 -	    handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
   1.752 +          cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
   1.753 +            handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
   1.754    in
   1.755      fix_shyps [] []
   1.756        (Thm {sign = sign, 
   1.757 -	    der = infer_derivs (Class_triv(thy,c), []), 
   1.758 -	    maxidx = maxidx, 
   1.759 -	    shyps = [], 
   1.760 -	    hyps = [], 
   1.761 -	    prop = t})
   1.762 +            der = infer_derivs (Class_triv(thy,c), []), 
   1.763 +            maxidx = maxidx, 
   1.764 +            shyps = [], 
   1.765 +            hyps = [], 
   1.766 +            prop = t})
   1.767    end;
   1.768  
   1.769  
   1.770 @@ -1055,10 +1055,10 @@
   1.771    let val tfrees = foldr add_term_tfree_names (hyps,[])
   1.772    in let val thm = (*no fix_shyps*)
   1.773      Thm{sign = sign, 
   1.774 -	der = infer_derivs (VarifyT, [der]), 
   1.775 -	maxidx = Int.max(0,maxidx), 
   1.776 -	shyps = shyps, 
   1.777 -	hyps = hyps,
   1.778 +        der = infer_derivs (VarifyT, [der]), 
   1.779 +        maxidx = Int.max(0,maxidx), 
   1.780 +        shyps = shyps, 
   1.781 +        hyps = hyps,
   1.782          prop = Type.varify(prop,tfrees)}
   1.783       in nodup_Vars thm "varifyT" end
   1.784  (* this nodup_Vars check can be removed if thms are guaranteed not to contain
   1.785 @@ -1070,10 +1070,10 @@
   1.786    let val prop' = Type.freeze prop
   1.787    in (*no fix_shyps*)
   1.788      Thm{sign = sign, 
   1.789 -	der = infer_derivs (FreezeT, [der]),
   1.790 -	maxidx = maxidx_of_term prop',
   1.791 -	shyps = shyps,
   1.792 -	hyps = hyps,
   1.793 +        der = infer_derivs (FreezeT, [der]),
   1.794 +        maxidx = maxidx_of_term prop',
   1.795 +        shyps = shyps,
   1.796 +        hyps = hyps,
   1.797          prop = prop'}
   1.798    end;
   1.799  
   1.800 @@ -1101,13 +1101,13 @@
   1.801        val (tpairs,As,B) = Logic.strip_horn prop
   1.802    in  (*no fix_shyps*)
   1.803        Thm{sign = merge_thm_sgs(state,orule),
   1.804 -	  der = infer_derivs (Lift_rule(ct_Bi, i), [der]),
   1.805 -	  maxidx = maxidx+smax+1,
   1.806 +          der = infer_derivs (Lift_rule(ct_Bi, i), [der]),
   1.807 +          maxidx = maxidx+smax+1,
   1.808            shyps=union_sort(sshyps,shyps), 
   1.809 -	  hyps=hyps, 
   1.810 +          hyps=hyps, 
   1.811            prop = Logic.rule_of (map (pairself lift_abs) tpairs,
   1.812 -				map lift_all As,    
   1.813 -				lift_all B)}
   1.814 +                                map lift_all As,    
   1.815 +                                lift_all B)}
   1.816    end;
   1.817  
   1.818  (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
   1.819 @@ -1117,15 +1117,15 @@
   1.820        fun newth (env as Envir.Envir{maxidx, ...}, tpairs) =
   1.821          fix_shyps [state] (env_codT env)
   1.822            (Thm{sign = sign, 
   1.823 -	       der = infer_derivs (Assumption (i, Some env), [der]),
   1.824 -	       maxidx = maxidx,
   1.825 -	       shyps = [],
   1.826 -	       hyps = hyps,
   1.827 -	       prop = 
   1.828 -	       if Envir.is_empty env then (*avoid wasted normalizations*)
   1.829 -		   Logic.rule_of (tpairs, Bs, C)
   1.830 -	       else (*normalize the new rule fully*)
   1.831 -		   Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))});
   1.832 +               der = infer_derivs (Assumption (i, Some env), [der]),
   1.833 +               maxidx = maxidx,
   1.834 +               shyps = [],
   1.835 +               hyps = hyps,
   1.836 +               prop = 
   1.837 +               if Envir.is_empty env then (*avoid wasted normalizations*)
   1.838 +                   Logic.rule_of (tpairs, Bs, C)
   1.839 +               else (*normalize the new rule fully*)
   1.840 +                   Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))});
   1.841        fun addprfs [] = Sequence.null
   1.842          | addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull
   1.843               (Sequence.mapp newth
   1.844 @@ -1141,11 +1141,11 @@
   1.845    in  if exists (op aconv) (Logic.assum_pairs Bi)
   1.846        then fix_shyps [state] []
   1.847               (Thm{sign = sign, 
   1.848 -		  der = infer_derivs (Assumption (i,None), [der]),
   1.849 -		  maxidx = maxidx,
   1.850 -		  shyps = [],
   1.851 -		  hyps = hyps,
   1.852 -		  prop = Logic.rule_of(tpairs, Bs, C)})
   1.853 +                  der = infer_derivs (Assumption (i,None), [der]),
   1.854 +                  maxidx = maxidx,
   1.855 +                  shyps = [],
   1.856 +                  hyps = hyps,
   1.857 +                  prop = Logic.rule_of(tpairs, Bs, C)})
   1.858        else  raise THM("eq_assumption", 0, [state])
   1.859    end;
   1.860  
   1.861 @@ -1172,12 +1172,12 @@
   1.862     | [] => (case cs inter_string freenames of
   1.863         a::_ => error ("Bound/Free variable clash: " ^ a)
   1.864       | [] => fix_shyps [state] []
   1.865 -		(Thm{sign = sign,
   1.866 -		     der = infer_derivs (Rename_params_rule(cs,i), [der]),
   1.867 -		     maxidx = maxidx,
   1.868 -		     shyps = [],
   1.869 -		     hyps = hyps,
   1.870 -		     prop = Logic.rule_of(tpairs, Bs@[newBi], C)}))
   1.871 +                (Thm{sign = sign,
   1.872 +                     der = infer_derivs (Rename_params_rule(cs,i), [der]),
   1.873 +                     maxidx = maxidx,
   1.874 +                     shyps = [],
   1.875 +                     hyps = hyps,
   1.876 +                     prop = Logic.rule_of(tpairs, Bs@[newBi], C)}))
   1.877    end;
   1.878  
   1.879  (*** Preservation of bound variable names ***)
   1.880 @@ -1273,7 +1273,7 @@
   1.881                          (eres_flg, orule, nsubgoal) =
   1.882   let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state
   1.883       and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps, 
   1.884 -	     prop=rprop,...} = orule
   1.885 +             prop=rprop,...} = orule
   1.886           (*How many hyps to skip over during normalization*)
   1.887       and nlift = Logic.count_prems(strip_all_body Bi,
   1.888                                     if eres_flg then ~1 else 0)
   1.889 @@ -1297,13 +1297,13 @@
   1.890               end
   1.891             val th = (*tuned fix_shyps*)
   1.892               Thm{sign = sign,
   1.893 -		 der = infer_derivs (Bicompose(match, eres_flg,
   1.894 -					       1 + length Bs, nsubgoal, env),
   1.895 -				     [rder,sder]),
   1.896 -		 maxidx = maxidx,
   1.897 -		 shyps = add_env_sorts (env, union_sort(rshyps,sshyps)),
   1.898 -		 hyps = union_term(rhyps,shyps),
   1.899 -		 prop = Logic.rule_of normp}
   1.900 +                 der = infer_derivs (Bicompose(match, eres_flg,
   1.901 +                                               1 + length Bs, nsubgoal, env),
   1.902 +                                     [rder,sder]),
   1.903 +                 maxidx = maxidx,
   1.904 +                 shyps = add_env_sorts (env, union_sort(rshyps,sshyps)),
   1.905 +                 hyps = union_term(rhyps,shyps),
   1.906 +                 prop = Logic.rule_of normp}
   1.907          in  cons(th, thq)  end  handle COMPOSE => thq
   1.908       val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop);
   1.909       val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn)
   1.910 @@ -1570,7 +1570,7 @@
   1.911           if (lhs = lhs0) orelse
   1.912              (lhs aconv Envir.norm_term (Envir.empty 0) lhs0)
   1.913           then (trace_thm "SUCCEEDED" thm; 
   1.914 -	       Some(shyps, hyps, maxidx, rhs, der::ders))
   1.915 +               Some(shyps, hyps, maxidx, rhs, der::ders))
   1.916           else err()
   1.917       | _ => err()
   1.918    end;
   1.919 @@ -1605,22 +1605,22 @@
   1.920              val hyps' = union_term(hyps,hypst);
   1.921              val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst));
   1.922              val maxidx' = maxidx_of_term prop'
   1.923 -            val ct' = Cterm{sign = signt,	(*used for deriv only*)
   1.924 -			    t = prop',
   1.925 -			    T = propT,
   1.926 -			    maxidx = maxidx'}
   1.927 -	    val der' = infer_derivs (RewriteC ct', [der])
   1.928 +            val ct' = Cterm{sign = signt,       (*used for deriv only*)
   1.929 +                            t = prop',
   1.930 +                            T = propT,
   1.931 +                            maxidx = maxidx'}
   1.932 +            val der' = infer_derivs (RewriteC ct', [der])
   1.933              val thm' = Thm{sign = signt, 
   1.934 -			   der = der',
   1.935 -			   shyps = shyps',
   1.936 -			   hyps = hyps',
   1.937 +                           der = der',
   1.938 +                           shyps = shyps',
   1.939 +                           hyps = hyps',
   1.940                             prop = prop',
   1.941 -			   maxidx = maxidx'}
   1.942 +                           maxidx = maxidx'}
   1.943              val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop')
   1.944          in if perm andalso not(termless(rhs',lhs')) then None else
   1.945             if Logic.count_prems(prop',0) = 0
   1.946             then (trace_thm "Rewriting:" thm'; 
   1.947 -		 Some(shyps', hyps', maxidx', rhs', der'::ders))
   1.948 +                 Some(shyps', hyps', maxidx', rhs', der'::ders))
   1.949             else (trace_thm "Trying to rewrite:" thm';
   1.950                   case prover mss thm' of
   1.951                     None       => (trace_thm "FAILED" thm'; None)
   1.952 @@ -1632,19 +1632,19 @@
   1.953              let val opt = rew rrule handle Pattern.MATCH => None
   1.954              in case opt of None => rews rrules | some => some end;
   1.955        fun sort_rrules rrs = let
   1.956 -	fun is_simple {thm as Thm{prop,...}, lhs, perm} = case prop of 
   1.957 -					Const("==",_) $ _ $ _ => true
   1.958 -					| _		      => false 
   1.959 -	fun sort []        (re1,re2) = re1 @ re2
   1.960 -	|   sort (rr::rrs) (re1,re2) = if is_simple rr 
   1.961 -				       then sort rrs (rr::re1,re2)
   1.962 -				       else sort rrs (re1,rr::re2)
   1.963 +        fun is_simple {thm as Thm{prop,...}, lhs, perm} = case prop of 
   1.964 +                                        Const("==",_) $ _ $ _ => true
   1.965 +                                        | _                   => false 
   1.966 +        fun sort []        (re1,re2) = re1 @ re2
   1.967 +        |   sort (rr::rrs) (re1,re2) = if is_simple rr 
   1.968 +                                       then sort rrs (rr::re1,re2)
   1.969 +                                       else sort rrs (re1,rr::re2)
   1.970        in sort rrs ([],[]) 
   1.971        end
   1.972    in case etat of
   1.973         Abs(_,_,body) $ u => Some(shypst, hypst, maxt, 
   1.974 -				 subst_bound (u, body),
   1.975 -				 ders)
   1.976 +                                 subst_bound (u, body),
   1.977 +                                 ders)
   1.978       | _                 => rews (sort_rrules (Net.match_term net etat))
   1.979    end;
   1.980  
   1.981 @@ -1664,16 +1664,16 @@
   1.982        val prop' = ren_inst(insts,rprop,rlhs,t);
   1.983        val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst))
   1.984        val maxidx' = maxidx_of_term prop'
   1.985 -      val ct' = Cterm{sign = signt,	(*used for deriv only*)
   1.986 -		      t = prop',
   1.987 -		      T = propT,
   1.988 -		      maxidx = maxidx'}
   1.989 +      val ct' = Cterm{sign = signt,     (*used for deriv only*)
   1.990 +                      t = prop',
   1.991 +                      T = propT,
   1.992 +                      maxidx = maxidx'}
   1.993        val thm' = Thm{sign = signt, 
   1.994 -		     der = infer_derivs (CongC ct', [der]),
   1.995 -		     shyps = shyps',
   1.996 -		     hyps = union_term(hyps,hypst),
   1.997 +                     der = infer_derivs (CongC ct', [der]),
   1.998 +                     shyps = shyps',
   1.999 +                     hyps = union_term(hyps,hypst),
  1.1000                       prop = prop',
  1.1001 -		     maxidx = maxidx'};
  1.1002 +                     maxidx = maxidx'};
  1.1003        val unit = trace_thm "Applying congruence rule" thm';
  1.1004        fun err() = error("Failed congruence proof!")
  1.1005  
  1.1006 @@ -1687,88 +1687,88 @@
  1.1007  
  1.1008  fun bottomc ((simprem,useprem),prover,sign) =
  1.1009   let fun botc fail mss trec =
  1.1010 -	  (case subc mss trec of
  1.1011 -	     some as Some(trec1) =>
  1.1012 -	       (case rewritec (prover,sign) mss trec1 of
  1.1013 -		  Some(trec2) => botc false mss trec2
  1.1014 -		| None => some)
  1.1015 -	   | None =>
  1.1016 -	       (case rewritec (prover,sign) mss trec of
  1.1017 -		  Some(trec2) => botc false mss trec2
  1.1018 -		| None => if fail then None else Some(trec)))
  1.1019 +          (case subc mss trec of
  1.1020 +             some as Some(trec1) =>
  1.1021 +               (case rewritec (prover,sign) mss trec1 of
  1.1022 +                  Some(trec2) => botc false mss trec2
  1.1023 +                | None => some)
  1.1024 +           | None =>
  1.1025 +               (case rewritec (prover,sign) mss trec of
  1.1026 +                  Some(trec2) => botc false mss trec2
  1.1027 +                | None => if fail then None else Some(trec)))
  1.1028  
  1.1029       and try_botc mss trec = (case botc true mss trec of
  1.1030 -				Some(trec1) => trec1
  1.1031 -			      | None => trec)
  1.1032 +                                Some(trec1) => trec1
  1.1033 +                              | None => trec)
  1.1034  
  1.1035       and subc (mss as Mss{net,congs,bounds,prems,mk_rews})
  1.1036 -	      (trec as (shyps,hyps,maxidx,t0,ders)) =
  1.1037 +              (trec as (shyps,hyps,maxidx,t0,ders)) =
  1.1038         (case t0 of
  1.1039 -	   Abs(a,T,t) =>
  1.1040 -	     let val b = variant bounds a
  1.1041 -		 val v = Free("." ^ b,T)
  1.1042 -		 val mss' = Mss{net=net, congs=congs, bounds=b::bounds,
  1.1043 -				prems=prems,mk_rews=mk_rews}
  1.1044 -	     in case botc true mss' 
  1.1045 -		       (shyps,hyps,maxidx,subst_bound (v,t),ders) of
  1.1046 -		  Some(shyps',hyps',maxidx',t',ders') =>
  1.1047 -		    Some(shyps', hyps', maxidx',
  1.1048 -			 Abs(a, T, abstract_over(v,t')),
  1.1049 -			 ders')
  1.1050 -		| None => None
  1.1051 -	     end
  1.1052 -	 | t$u => (case t of
  1.1053 -	     Const("==>",_)$s  => Some(impc(shyps,hyps,maxidx,s,u,mss,ders))
  1.1054 -	   | Abs(_,_,body) =>
  1.1055 -	       let val trec = (shyps,hyps,maxidx,subst_bound (u,body),ders)
  1.1056 -	       in case subc mss trec of
  1.1057 -		    None => Some(trec)
  1.1058 -		  | trec => trec
  1.1059 -	       end
  1.1060 -	   | _  =>
  1.1061 -	       let fun appc() =
  1.1062 -		     (case botc true mss (shyps,hyps,maxidx,t,ders) of
  1.1063 -			Some(shyps1,hyps1,maxidx1,t1,ders1) =>
  1.1064 -			  (case botc true mss (shyps1,hyps1,maxidx,u,ders1) of
  1.1065 -			     Some(shyps2,hyps2,maxidx2,u1,ders2) =>
  1.1066 -			       Some(shyps2, hyps2, Int.max(maxidx1,maxidx2),
  1.1067 -				    t1$u1, ders2)
  1.1068 -			   | None =>
  1.1069 -			       Some(shyps1, hyps1, Int.max(maxidx1,maxidx), t1$u,
  1.1070 -				    ders1))
  1.1071 -		      | None =>
  1.1072 -			  (case botc true mss (shyps,hyps,maxidx,u,ders) of
  1.1073 -			     Some(shyps1,hyps1,maxidx1,u1,ders1) =>
  1.1074 -			       Some(shyps1, hyps1, Int.max(maxidx,maxidx1), 
  1.1075 -				    t$u1, ders1)
  1.1076 -			   | None => None))
  1.1077 -		   val (h,ts) = strip_comb t
  1.1078 -	       in case h of
  1.1079 -		    Const(a,_) =>
  1.1080 -		      (case assoc_string(congs,a) of
  1.1081 -			 None => appc()
  1.1082 -		       | Some(cong) => (congc (prover mss,sign) cong trec
  1.1083 +           Abs(a,T,t) =>
  1.1084 +             let val b = variant bounds a
  1.1085 +                 val v = Free("." ^ b,T)
  1.1086 +                 val mss' = Mss{net=net, congs=congs, bounds=b::bounds,
  1.1087 +                                prems=prems,mk_rews=mk_rews}
  1.1088 +             in case botc true mss' 
  1.1089 +                       (shyps,hyps,maxidx,subst_bound (v,t),ders) of
  1.1090 +                  Some(shyps',hyps',maxidx',t',ders') =>
  1.1091 +                    Some(shyps', hyps', maxidx',
  1.1092 +                         Abs(a, T, abstract_over(v,t')),
  1.1093 +                         ders')
  1.1094 +                | None => None
  1.1095 +             end
  1.1096 +         | t$u => (case t of
  1.1097 +             Const("==>",_)$s  => Some(impc(shyps,hyps,maxidx,s,u,mss,ders))
  1.1098 +           | Abs(_,_,body) =>
  1.1099 +               let val trec = (shyps,hyps,maxidx,subst_bound (u,body),ders)
  1.1100 +               in case subc mss trec of
  1.1101 +                    None => Some(trec)
  1.1102 +                  | trec => trec
  1.1103 +               end
  1.1104 +           | _  =>
  1.1105 +               let fun appc() =
  1.1106 +                     (case botc true mss (shyps,hyps,maxidx,t,ders) of
  1.1107 +                        Some(shyps1,hyps1,maxidx1,t1,ders1) =>
  1.1108 +                          (case botc true mss (shyps1,hyps1,maxidx,u,ders1) of
  1.1109 +                             Some(shyps2,hyps2,maxidx2,u1,ders2) =>
  1.1110 +                               Some(shyps2, hyps2, Int.max(maxidx1,maxidx2),
  1.1111 +                                    t1$u1, ders2)
  1.1112 +                           | None =>
  1.1113 +                               Some(shyps1, hyps1, Int.max(maxidx1,maxidx), t1$u,
  1.1114 +                                    ders1))
  1.1115 +                      | None =>
  1.1116 +                          (case botc true mss (shyps,hyps,maxidx,u,ders) of
  1.1117 +                             Some(shyps1,hyps1,maxidx1,u1,ders1) =>
  1.1118 +                               Some(shyps1, hyps1, Int.max(maxidx,maxidx1), 
  1.1119 +                                    t$u1, ders1)
  1.1120 +                           | None => None))
  1.1121 +                   val (h,ts) = strip_comb t
  1.1122 +               in case h of
  1.1123 +                    Const(a,_) =>
  1.1124 +                      (case assoc_string(congs,a) of
  1.1125 +                         None => appc()
  1.1126 +                       | Some(cong) => (congc (prover mss,sign) cong trec
  1.1127                                          handle Pattern.MATCH => appc() ) )
  1.1128 -		  | _ => appc()
  1.1129 -	       end)
  1.1130 -	 | _ => None)
  1.1131 +                  | _ => appc()
  1.1132 +               end)
  1.1133 +         | _ => None)
  1.1134  
  1.1135       and impc(shyps, hyps, maxidx, s, u, mss as Mss{mk_rews,...}, ders) =
  1.1136         let val (shyps1,hyps1,_,s1,ders1) =
  1.1137 -	     if simprem then try_botc mss (shyps,hyps,maxidx,s,ders)
  1.1138 -	                else (shyps,hyps,0,s,ders);
  1.1139 -	   val maxidx1 = maxidx_of_term s1
  1.1140 -	   val mss1 =
  1.1141 -	     if not useprem orelse maxidx1 <> ~1 then mss
  1.1142 -	     else let val thm = assume (Cterm{sign=sign, t=s1, 
  1.1143 -					      T=propT, maxidx=maxidx1})
  1.1144 -		  in add_simps(add_prems(mss,[thm]), mk_rews thm) end
  1.1145 -	   val (shyps2,hyps2,maxidx2,u1,ders2) = 
  1.1146 -	       try_botc mss1 (shyps1,hyps1,maxidx,u,ders1)
  1.1147 -	   val hyps3 = if gen_mem (op aconv) (s1, hyps1) 
  1.1148 -		       then hyps2 else hyps2\s1
  1.1149 +             if simprem then try_botc mss (shyps,hyps,maxidx,s,ders)
  1.1150 +                        else (shyps,hyps,0,s,ders);
  1.1151 +           val maxidx1 = maxidx_of_term s1
  1.1152 +           val mss1 =
  1.1153 +             if not useprem orelse maxidx1 <> ~1 then mss
  1.1154 +             else let val thm = assume (Cterm{sign=sign, t=s1, 
  1.1155 +                                              T=propT, maxidx=maxidx1})
  1.1156 +                  in add_simps(add_prems(mss,[thm]), mk_rews thm) end
  1.1157 +           val (shyps2,hyps2,maxidx2,u1,ders2) = 
  1.1158 +               try_botc mss1 (shyps1,hyps1,maxidx,u,ders1)
  1.1159 +           val hyps3 = if gen_mem (op aconv) (s1, hyps1) 
  1.1160 +                       then hyps2 else hyps2\s1
  1.1161         in (shyps2, hyps3, Int.max(maxidx1,maxidx2), 
  1.1162 -	   Logic.mk_implies(s1,u1), ders2) 
  1.1163 +           Logic.mk_implies(s1,u1), ders2) 
  1.1164         end
  1.1165  
  1.1166   in try_botc end;
  1.1167 @@ -1785,34 +1785,34 @@
  1.1168    let val {sign, t, T, maxidx} = rep_cterm ct;
  1.1169        val (shyps,hyps,maxu,u,ders) =
  1.1170          bottomc (mode,prover,sign) mss 
  1.1171 -	        (add_term_sorts(t,[]), [], maxidx, t, []);
  1.1172 +                (add_term_sorts(t,[]), [], maxidx, t, []);
  1.1173        val prop = Logic.mk_equals(t,u)
  1.1174    in
  1.1175        Thm{sign = sign, 
  1.1176 -	  der = infer_derivs (Rewrite_cterm ct, ders),
  1.1177 -	  maxidx = Int.max (maxidx,maxu),
  1.1178 -	  shyps = shyps, 
  1.1179 -	  hyps = hyps, 
  1.1180 +          der = infer_derivs (Rewrite_cterm ct, ders),
  1.1181 +          maxidx = Int.max (maxidx,maxu),
  1.1182 +          shyps = shyps, 
  1.1183 +          hyps = hyps, 
  1.1184            prop = prop}
  1.1185    end
  1.1186  
  1.1187  
  1.1188  fun invoke_oracle (thy, sign, exn) =
  1.1189      case #oraopt(rep_theory thy) of
  1.1190 -	None => raise THM ("No oracle in supplied theory", 0, [])
  1.1191 +        None => raise THM ("No oracle in supplied theory", 0, [])
  1.1192        | Some oracle => 
  1.1193 -	    let val sign' = Sign.merge(sign_of thy, sign)
  1.1194 -		val (prop, T, maxidx) = 
  1.1195 -		    Sign.certify_term sign' (oracle (sign', exn))
  1.1196 +            let val sign' = Sign.merge(sign_of thy, sign)
  1.1197 +                val (prop, T, maxidx) = 
  1.1198 +                    Sign.certify_term sign' (oracle (sign', exn))
  1.1199              in if T<>propT then
  1.1200                    raise THM("Oracle's result must have type prop", 0, [])
  1.1201 -	       else fix_shyps [] []
  1.1202 -		     (Thm {sign = sign', 
  1.1203 -			   der = Join (Oracle(thy,sign,exn), []),
  1.1204 -			   maxidx = maxidx,
  1.1205 -			   shyps = [], 
  1.1206 -			   hyps = [], 
  1.1207 -			   prop = prop})
  1.1208 +               else fix_shyps [] []
  1.1209 +                     (Thm {sign = sign', 
  1.1210 +                           der = Join (Oracle(thy,sign,exn), []),
  1.1211 +                           maxidx = maxidx,
  1.1212 +                           shyps = [], 
  1.1213 +                           hyps = [], 
  1.1214 +                           prop = prop})
  1.1215              end;
  1.1216  
  1.1217  end;