src/HOL/Import/shuffler.ML
changeset 21588 cd0dc678a205
parent 21078 101aefd61aac
child 22578 b0eb5652f210
     1.1 --- a/src/HOL/Import/shuffler.ML	Wed Nov 29 15:44:46 2006 +0100
     1.2 +++ b/src/HOL/Import/shuffler.ML	Wed Nov 29 15:44:51 2006 +0100
     1.3 @@ -38,21 +38,21 @@
     1.4  val message = if_debug writeln
     1.5  
     1.6  (*Prints exceptions readably to users*)
     1.7 -fun print_sign_exn_unit sign e = 
     1.8 +fun print_sign_exn_unit sign e =
     1.9    case e of
    1.10       THM (msg,i,thms) =>
    1.11 -	 (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
    1.12 -	  List.app print_thm thms)
    1.13 +         (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
    1.14 +          List.app print_thm thms)
    1.15     | THEORY (msg,thys) =>
    1.16 -	 (writeln ("Exception THEORY raised:\n" ^ msg);
    1.17 -	  List.app (writeln o Context.str_of_thy) thys)
    1.18 +         (writeln ("Exception THEORY raised:\n" ^ msg);
    1.19 +          List.app (writeln o Context.str_of_thy) thys)
    1.20     | TERM (msg,ts) =>
    1.21 -	 (writeln ("Exception TERM raised:\n" ^ msg);
    1.22 -	  List.app (writeln o Sign.string_of_term sign) ts)
    1.23 +         (writeln ("Exception TERM raised:\n" ^ msg);
    1.24 +          List.app (writeln o Sign.string_of_term sign) ts)
    1.25     | TYPE (msg,Ts,ts) =>
    1.26 -	 (writeln ("Exception TYPE raised:\n" ^ msg);
    1.27 -	  List.app (writeln o Sign.string_of_typ sign) Ts;
    1.28 -	  List.app (writeln o Sign.string_of_term sign) ts)
    1.29 +         (writeln ("Exception TYPE raised:\n" ^ msg);
    1.30 +          List.app (writeln o Sign.string_of_typ sign) Ts;
    1.31 +          List.app (writeln o Sign.string_of_term sign) ts)
    1.32     | e => raise e
    1.33  
    1.34  (*Prints an exception, then fails*)
    1.35 @@ -63,14 +63,14 @@
    1.36  
    1.37  fun mk_meta_eq th =
    1.38      (case concl_of th of
    1.39 -	 Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection
    1.40 +         Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection
    1.41         | Const("==",_) $ _ $ _ => th
    1.42         | _ => raise THM("Not an equality",0,[th]))
    1.43      handle _ => raise THM("Couldn't make meta equality",0,[th])
    1.44 -				   
    1.45 +
    1.46  fun mk_obj_eq th =
    1.47      (case concl_of th of
    1.48 -	 Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th
    1.49 +         Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th
    1.50         | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
    1.51         | _ => raise THM("Not an equality",0,[th]))
    1.52      handle _ => raise THM("Couldn't make object equality",0,[th])
    1.53 @@ -85,113 +85,113 @@
    1.54  fun merge _ = Library.gen_union Thm.eq_thm
    1.55  fun print _ thms =
    1.56      Pretty.writeln (Pretty.big_list "Shuffle theorems:"
    1.57 -				    (map Display.pretty_thm thms))
    1.58 +                                    (map Display.pretty_thm thms))
    1.59  end
    1.60  
    1.61  structure ShuffleData = TheoryDataFun(ShuffleDataArgs)
    1.62  
    1.63  val weaken =
    1.64      let
    1.65 -	val cert = cterm_of ProtoPure.thy
    1.66 -	val P = Free("P",propT)
    1.67 -	val Q = Free("Q",propT)
    1.68 -	val PQ = Logic.mk_implies(P,Q)
    1.69 -	val PPQ = Logic.mk_implies(P,PQ)
    1.70 -	val cP = cert P
    1.71 -	val cQ = cert Q
    1.72 -	val cPQ = cert PQ
    1.73 -	val cPPQ = cert PPQ
    1.74 -	val th1 = assume cPQ |> implies_intr_list [cPQ,cP]
    1.75 -	val th3 = assume cP
    1.76 -	val th4 = implies_elim_list (assume cPPQ) [th3,th3]
    1.77 -				    |> implies_intr_list [cPPQ,cP]
    1.78 +        val cert = cterm_of ProtoPure.thy
    1.79 +        val P = Free("P",propT)
    1.80 +        val Q = Free("Q",propT)
    1.81 +        val PQ = Logic.mk_implies(P,Q)
    1.82 +        val PPQ = Logic.mk_implies(P,PQ)
    1.83 +        val cP = cert P
    1.84 +        val cQ = cert Q
    1.85 +        val cPQ = cert PQ
    1.86 +        val cPPQ = cert PPQ
    1.87 +        val th1 = assume cPQ |> implies_intr_list [cPQ,cP]
    1.88 +        val th3 = assume cP
    1.89 +        val th4 = implies_elim_list (assume cPPQ) [th3,th3]
    1.90 +                                    |> implies_intr_list [cPPQ,cP]
    1.91      in
    1.92 -	equal_intr th4 th1 |> standard
    1.93 +        equal_intr th4 th1 |> standard
    1.94      end
    1.95  
    1.96  val imp_comm =
    1.97      let
    1.98 -	val cert = cterm_of ProtoPure.thy
    1.99 -	val P = Free("P",propT)
   1.100 -	val Q = Free("Q",propT)
   1.101 -	val R = Free("R",propT)
   1.102 -	val PQR = Logic.mk_implies(P,Logic.mk_implies(Q,R))
   1.103 -	val QPR = Logic.mk_implies(Q,Logic.mk_implies(P,R))
   1.104 -	val cP = cert P
   1.105 -	val cQ = cert Q
   1.106 -	val cPQR = cert PQR
   1.107 -	val cQPR = cert QPR
   1.108 -	val th1 = implies_elim_list (assume cPQR) [assume cP,assume cQ]
   1.109 -				    |> implies_intr_list [cPQR,cQ,cP]
   1.110 -	val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP]
   1.111 -				    |> implies_intr_list [cQPR,cP,cQ]
   1.112 +        val cert = cterm_of ProtoPure.thy
   1.113 +        val P = Free("P",propT)
   1.114 +        val Q = Free("Q",propT)
   1.115 +        val R = Free("R",propT)
   1.116 +        val PQR = Logic.mk_implies(P,Logic.mk_implies(Q,R))
   1.117 +        val QPR = Logic.mk_implies(Q,Logic.mk_implies(P,R))
   1.118 +        val cP = cert P
   1.119 +        val cQ = cert Q
   1.120 +        val cPQR = cert PQR
   1.121 +        val cQPR = cert QPR
   1.122 +        val th1 = implies_elim_list (assume cPQR) [assume cP,assume cQ]
   1.123 +                                    |> implies_intr_list [cPQR,cQ,cP]
   1.124 +        val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP]
   1.125 +                                    |> implies_intr_list [cQPR,cP,cQ]
   1.126      in
   1.127 -	equal_intr th1 th2 |> standard
   1.128 +        equal_intr th1 th2 |> standard
   1.129      end
   1.130  
   1.131  val def_norm =
   1.132      let
   1.133 -	val cert = cterm_of ProtoPure.thy
   1.134 -	val aT = TFree("'a",[])
   1.135 -	val bT = TFree("'b",[])
   1.136 -	val v = Free("v",aT)
   1.137 -	val P = Free("P",aT-->bT)
   1.138 -	val Q = Free("Q",aT-->bT)
   1.139 -	val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0)))
   1.140 -	val cPQ = cert (Logic.mk_equals(P,Q))
   1.141 -	val cv = cert v
   1.142 -	val rew = assume cvPQ
   1.143 -			 |> forall_elim cv
   1.144 -			 |> abstract_rule "v" cv
   1.145 -	val (lhs,rhs) = Logic.dest_equals(concl_of rew)
   1.146 -	val th1 = transitive (transitive
   1.147 -				  (eta_conversion (cert lhs) |> symmetric)
   1.148 -				  rew)
   1.149 -			     (eta_conversion (cert rhs))
   1.150 -			     |> implies_intr cvPQ
   1.151 -	val th2 = combination (assume cPQ) (reflexive cv)
   1.152 -			      |> forall_intr cv
   1.153 -			      |> implies_intr cPQ
   1.154 +        val cert = cterm_of ProtoPure.thy
   1.155 +        val aT = TFree("'a",[])
   1.156 +        val bT = TFree("'b",[])
   1.157 +        val v = Free("v",aT)
   1.158 +        val P = Free("P",aT-->bT)
   1.159 +        val Q = Free("Q",aT-->bT)
   1.160 +        val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0)))
   1.161 +        val cPQ = cert (Logic.mk_equals(P,Q))
   1.162 +        val cv = cert v
   1.163 +        val rew = assume cvPQ
   1.164 +                         |> forall_elim cv
   1.165 +                         |> abstract_rule "v" cv
   1.166 +        val (lhs,rhs) = Logic.dest_equals(concl_of rew)
   1.167 +        val th1 = transitive (transitive
   1.168 +                                  (eta_conversion (cert lhs) |> symmetric)
   1.169 +                                  rew)
   1.170 +                             (eta_conversion (cert rhs))
   1.171 +                             |> implies_intr cvPQ
   1.172 +        val th2 = combination (assume cPQ) (reflexive cv)
   1.173 +                              |> forall_intr cv
   1.174 +                              |> implies_intr cPQ
   1.175      in
   1.176 -	equal_intr th1 th2 |> standard
   1.177 +        equal_intr th1 th2 |> standard
   1.178      end
   1.179  
   1.180  val all_comm =
   1.181      let
   1.182 -	val cert = cterm_of ProtoPure.thy
   1.183 -	val xT = TFree("'a",[])
   1.184 -	val yT = TFree("'b",[])
   1.185 -	val P = Free("P",xT-->yT-->propT)
   1.186 -	val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))
   1.187 -	val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1))))
   1.188 -	val cl = cert lhs
   1.189 -	val cr = cert rhs
   1.190 -	val cx = cert (Free("x",xT))
   1.191 -	val cy = cert (Free("y",yT))
   1.192 -	val th1 = assume cr
   1.193 -			 |> forall_elim_list [cy,cx]
   1.194 -			 |> forall_intr_list [cx,cy]
   1.195 -			 |> implies_intr cr
   1.196 -	val th2 = assume cl
   1.197 -			 |> forall_elim_list [cx,cy]
   1.198 -			 |> forall_intr_list [cy,cx]
   1.199 -			 |> implies_intr cl
   1.200 +        val cert = cterm_of ProtoPure.thy
   1.201 +        val xT = TFree("'a",[])
   1.202 +        val yT = TFree("'b",[])
   1.203 +        val P = Free("P",xT-->yT-->propT)
   1.204 +        val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))
   1.205 +        val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1))))
   1.206 +        val cl = cert lhs
   1.207 +        val cr = cert rhs
   1.208 +        val cx = cert (Free("x",xT))
   1.209 +        val cy = cert (Free("y",yT))
   1.210 +        val th1 = assume cr
   1.211 +                         |> forall_elim_list [cy,cx]
   1.212 +                         |> forall_intr_list [cx,cy]
   1.213 +                         |> implies_intr cr
   1.214 +        val th2 = assume cl
   1.215 +                         |> forall_elim_list [cx,cy]
   1.216 +                         |> forall_intr_list [cy,cx]
   1.217 +                         |> implies_intr cl
   1.218      in
   1.219 -	equal_intr th1 th2 |> standard
   1.220 +        equal_intr th1 th2 |> standard
   1.221      end
   1.222  
   1.223  val equiv_comm =
   1.224      let
   1.225 -	val cert = cterm_of ProtoPure.thy
   1.226 -	val T    = TFree("'a",[])
   1.227 -	val t    = Free("t",T)
   1.228 -	val u    = Free("u",T)
   1.229 -	val ctu  = cert (Logic.mk_equals(t,u))
   1.230 -	val cut  = cert (Logic.mk_equals(u,t))
   1.231 -	val th1  = assume ctu |> symmetric |> implies_intr ctu
   1.232 -	val th2  = assume cut |> symmetric |> implies_intr cut
   1.233 +        val cert = cterm_of ProtoPure.thy
   1.234 +        val T    = TFree("'a",[])
   1.235 +        val t    = Free("t",T)
   1.236 +        val u    = Free("u",T)
   1.237 +        val ctu  = cert (Logic.mk_equals(t,u))
   1.238 +        val cut  = cert (Logic.mk_equals(u,t))
   1.239 +        val th1  = assume ctu |> symmetric |> implies_intr ctu
   1.240 +        val th2  = assume cut |> symmetric |> implies_intr cut
   1.241      in
   1.242 -	equal_intr th1 th2 |> standard
   1.243 +        equal_intr th1 th2 |> standard
   1.244      end
   1.245  
   1.246  (* This simplification procedure rewrites !!x y. P x y
   1.247 @@ -203,82 +203,82 @@
   1.248  exception RESULT of int
   1.249  
   1.250  fun find_bound n (Bound i) = if i = n then raise RESULT 0
   1.251 -			     else if i = n+1 then raise RESULT 1
   1.252 -			     else ()
   1.253 +                             else if i = n+1 then raise RESULT 1
   1.254 +                             else ()
   1.255    | find_bound n (t $ u) = (find_bound n t; find_bound n u)
   1.256    | find_bound n (Abs(_,_,t)) = find_bound (n+1) t
   1.257    | find_bound _ _ = ()
   1.258  
   1.259  fun swap_bound n (Bound i) = if i = n then Bound (n+1)
   1.260 -			     else if i = n+1 then Bound n
   1.261 -			     else Bound i
   1.262 +                             else if i = n+1 then Bound n
   1.263 +                             else Bound i
   1.264    | swap_bound n (t $ u) = (swap_bound n t $ swap_bound n u)
   1.265    | swap_bound n (Abs(x,xT,t)) = Abs(x,xT,swap_bound (n+1) t)
   1.266    | swap_bound n t = t
   1.267  
   1.268  fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t =
   1.269      let
   1.270 -	val lhs = list_all ([xv,yv],t)
   1.271 -	val rhs = list_all ([yv,xv],swap_bound 0 t)
   1.272 -	val rew = Logic.mk_equals (lhs,rhs)
   1.273 -	val init = trivial (cterm_of thy rew)
   1.274 +        val lhs = list_all ([xv,yv],t)
   1.275 +        val rhs = list_all ([yv,xv],swap_bound 0 t)
   1.276 +        val rew = Logic.mk_equals (lhs,rhs)
   1.277 +        val init = trivial (cterm_of thy rew)
   1.278      in
   1.279 -	(all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
   1.280 +        (all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
   1.281      end
   1.282  
   1.283  fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
   1.284      let
   1.285 -	val res = (find_bound 0 body;2) handle RESULT i => i
   1.286 +        val res = (find_bound 0 body;2) handle RESULT i => i
   1.287      in
   1.288 -	case res of
   1.289 -	    0 => SOME (rew_th thy (x,xT) (y,yT) body)
   1.290 -	  | 1 => if string_ord(y,x) = LESS
   1.291 -		 then
   1.292 -		     let
   1.293 -			 val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body)))
   1.294 -			 val t_th    = reflexive (cterm_of thy t)
   1.295 -			 val newt_th = reflexive (cterm_of thy newt)
   1.296 -		     in
   1.297 -			 SOME (transitive t_th newt_th)
   1.298 -		     end
   1.299 -		 else NONE
   1.300 -	  | _ => error "norm_term (quant_rewrite) internal error"
   1.301 +        case res of
   1.302 +            0 => SOME (rew_th thy (x,xT) (y,yT) body)
   1.303 +          | 1 => if string_ord(y,x) = LESS
   1.304 +                 then
   1.305 +                     let
   1.306 +                         val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body)))
   1.307 +                         val t_th    = reflexive (cterm_of thy t)
   1.308 +                         val newt_th = reflexive (cterm_of thy newt)
   1.309 +                     in
   1.310 +                         SOME (transitive t_th newt_th)
   1.311 +                     end
   1.312 +                 else NONE
   1.313 +          | _ => error "norm_term (quant_rewrite) internal error"
   1.314       end
   1.315    | quant_rewrite _ _ _ = (warning "quant_rewrite: Unknown lhs"; NONE)
   1.316  
   1.317  fun freeze_thaw_term t =
   1.318      let
   1.319 -	val tvars = term_tvars t
   1.320 -	val tfree_names = add_term_tfree_names(t,[])
   1.321 -	val (type_inst,_) =
   1.322 -	    Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
   1.323 -		      let
   1.324 -			  val v' = Name.variant used v
   1.325 -		      in
   1.326 -			  ((w,TFree(v',S))::inst,v'::used)
   1.327 -		      end)
   1.328 -		  (([],tfree_names),tvars)
   1.329 -	val t' = subst_TVars type_inst t
   1.330 +        val tvars = term_tvars t
   1.331 +        val tfree_names = add_term_tfree_names(t,[])
   1.332 +        val (type_inst,_) =
   1.333 +            Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
   1.334 +                      let
   1.335 +                          val v' = Name.variant used v
   1.336 +                      in
   1.337 +                          ((w,TFree(v',S))::inst,v'::used)
   1.338 +                      end)
   1.339 +                  (([],tfree_names),tvars)
   1.340 +        val t' = subst_TVars type_inst t
   1.341      in
   1.342 -	(t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))
   1.343 -		  | _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
   1.344 +        (t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))
   1.345 +                  | _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
   1.346      end
   1.347  
   1.348  fun inst_tfrees thy [] thm = thm
   1.349 -  | inst_tfrees thy ((name,U)::rest) thm = 
   1.350 +  | inst_tfrees thy ((name,U)::rest) thm =
   1.351      let
   1.352 -	val cU = ctyp_of thy U
   1.353 -	val tfrees = add_term_tfrees (prop_of thm,[])
   1.354 -	val (rens, thm') = Thm.varifyT'
   1.355 +        val cU = ctyp_of thy U
   1.356 +        val tfrees = add_term_tfrees (prop_of thm,[])
   1.357 +        val (rens, thm') = Thm.varifyT'
   1.358      (remove (op = o apsnd fst) name tfrees) thm
   1.359 -	val mid = 
   1.360 -	    case rens of
   1.361 -		[] => thm'
   1.362 -	      | [((_, S), idx)] => instantiate
   1.363 +        val mid =
   1.364 +            case rens of
   1.365 +                [] => thm'
   1.366 +              | [((_, S), idx)] => instantiate
   1.367              ([(ctyp_of thy (TVar (idx, S)), cU)], []) thm'
   1.368 -	      | _ => error "Shuffler.inst_tfrees internal error"
   1.369 +              | _ => error "Shuffler.inst_tfrees internal error"
   1.370      in
   1.371 -	inst_tfrees thy rest mid
   1.372 +        inst_tfrees thy rest mid
   1.373      end
   1.374  
   1.375  fun is_Abs (Abs _) = true
   1.376 @@ -286,65 +286,65 @@
   1.377  
   1.378  fun eta_redex (t $ Bound 0) =
   1.379      let
   1.380 -	fun free n (Bound i) = i = n
   1.381 -	  | free n (t $ u) = free n t orelse free n u
   1.382 -	  | free n (Abs(_,_,t)) = free (n+1) t
   1.383 -	  | free n _ = false
   1.384 +        fun free n (Bound i) = i = n
   1.385 +          | free n (t $ u) = free n t orelse free n u
   1.386 +          | free n (Abs(_,_,t)) = free (n+1) t
   1.387 +          | free n _ = false
   1.388      in
   1.389 -	not (free 0 t)
   1.390 +        not (free 0 t)
   1.391      end
   1.392    | eta_redex _ = false
   1.393  
   1.394  fun eta_contract thy assumes origt =
   1.395      let
   1.396 -	val (typet,Tinst) = freeze_thaw_term origt
   1.397 -	val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
   1.398 -	val final = inst_tfrees thy Tinst o thaw
   1.399 -	val t = #1 (Logic.dest_equals (prop_of init))
   1.400 -	val _ =
   1.401 -	    let
   1.402 -		val lhs = #1 (Logic.dest_equals (prop_of (final init)))
   1.403 -	    in
   1.404 -		if not (lhs aconv origt)
   1.405 -		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
   1.406 -		      writeln (string_of_cterm (cterm_of thy origt));
   1.407 -		      writeln (string_of_cterm (cterm_of thy lhs));
   1.408 -		      writeln (string_of_cterm (cterm_of thy typet));
   1.409 -		      writeln (string_of_cterm (cterm_of thy t));
   1.410 -		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
   1.411 -		      writeln "done")
   1.412 -		else ()
   1.413 -	    end
   1.414 +        val (typet,Tinst) = freeze_thaw_term origt
   1.415 +        val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
   1.416 +        val final = inst_tfrees thy Tinst o thaw
   1.417 +        val t = #1 (Logic.dest_equals (prop_of init))
   1.418 +        val _ =
   1.419 +            let
   1.420 +                val lhs = #1 (Logic.dest_equals (prop_of (final init)))
   1.421 +            in
   1.422 +                if not (lhs aconv origt)
   1.423 +                then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
   1.424 +                      writeln (string_of_cterm (cterm_of thy origt));
   1.425 +                      writeln (string_of_cterm (cterm_of thy lhs));
   1.426 +                      writeln (string_of_cterm (cterm_of thy typet));
   1.427 +                      writeln (string_of_cterm (cterm_of thy t));
   1.428 +                      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
   1.429 +                      writeln "done")
   1.430 +                else ()
   1.431 +            end
   1.432      in
   1.433 -	case t of
   1.434 -	    Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) =>
   1.435 -	    ((if eta_redex P andalso eta_redex Q
   1.436 -	      then
   1.437 -		  let
   1.438 -		      val cert = cterm_of thy
   1.439 -		      val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
   1.440 -		      val cv = cert v
   1.441 -		      val ct = cert t
   1.442 -		      val th = (assume ct)
   1.443 -				   |> forall_elim cv
   1.444 -				   |> abstract_rule x cv
   1.445 -		      val ext_th = eta_conversion (cert (Abs(x,xT,P)))
   1.446 -		      val th' = transitive (symmetric ext_th) th
   1.447 -		      val cu = cert (prop_of th')
   1.448 -		      val uth = combination (assume cu) (reflexive cv)
   1.449 -		      val uth' = (beta_conversion false (cert (Abs(x,xT,Q) $ v)))
   1.450 -				     |> transitive uth
   1.451 -				     |> forall_intr cv
   1.452 -				     |> implies_intr cu
   1.453 -		      val rew_th = equal_intr (th' |> implies_intr ct) uth'
   1.454 -		      val res = final rew_th
   1.455 -		      val lhs = (#1 (Logic.dest_equals (prop_of res)))
   1.456 -		  in
   1.457 -		       SOME res
   1.458 -		  end
   1.459 -	      else NONE)
   1.460 -	     handle e => OldGoals.print_exn e)
   1.461 -	  | _ => NONE
   1.462 +        case t of
   1.463 +            Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) =>
   1.464 +            ((if eta_redex P andalso eta_redex Q
   1.465 +              then
   1.466 +                  let
   1.467 +                      val cert = cterm_of thy
   1.468 +                      val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
   1.469 +                      val cv = cert v
   1.470 +                      val ct = cert t
   1.471 +                      val th = (assume ct)
   1.472 +                                   |> forall_elim cv
   1.473 +                                   |> abstract_rule x cv
   1.474 +                      val ext_th = eta_conversion (cert (Abs(x,xT,P)))
   1.475 +                      val th' = transitive (symmetric ext_th) th
   1.476 +                      val cu = cert (prop_of th')
   1.477 +                      val uth = combination (assume cu) (reflexive cv)
   1.478 +                      val uth' = (beta_conversion false (cert (Abs(x,xT,Q) $ v)))
   1.479 +                                     |> transitive uth
   1.480 +                                     |> forall_intr cv
   1.481 +                                     |> implies_intr cu
   1.482 +                      val rew_th = equal_intr (th' |> implies_intr ct) uth'
   1.483 +                      val res = final rew_th
   1.484 +                      val lhs = (#1 (Logic.dest_equals (prop_of res)))
   1.485 +                  in
   1.486 +                       SOME res
   1.487 +                  end
   1.488 +              else NONE)
   1.489 +             handle e => OldGoals.print_exn e)
   1.490 +          | _ => NONE
   1.491         end
   1.492  
   1.493  fun beta_fun thy assume t =
   1.494 @@ -354,62 +354,62 @@
   1.495  
   1.496  fun equals_fun thy assume t =
   1.497      case t of
   1.498 -	Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
   1.499 +        Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
   1.500        | _ => NONE
   1.501  
   1.502  fun eta_expand thy assumes origt =
   1.503      let
   1.504 -	val (typet,Tinst) = freeze_thaw_term origt
   1.505 -	val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
   1.506 -	val final = inst_tfrees thy Tinst o thaw
   1.507 -	val t = #1 (Logic.dest_equals (prop_of init))
   1.508 -	val _ =
   1.509 -	    let
   1.510 -		val lhs = #1 (Logic.dest_equals (prop_of (final init)))
   1.511 -	    in
   1.512 -		if not (lhs aconv origt)
   1.513 -		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
   1.514 -		      writeln (string_of_cterm (cterm_of thy origt));
   1.515 -		      writeln (string_of_cterm (cterm_of thy lhs));
   1.516 -		      writeln (string_of_cterm (cterm_of thy typet));
   1.517 -		      writeln (string_of_cterm (cterm_of thy t));
   1.518 -		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
   1.519 -		      writeln "done")
   1.520 -		else ()
   1.521 -	    end
   1.522 +        val (typet,Tinst) = freeze_thaw_term origt
   1.523 +        val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
   1.524 +        val final = inst_tfrees thy Tinst o thaw
   1.525 +        val t = #1 (Logic.dest_equals (prop_of init))
   1.526 +        val _ =
   1.527 +            let
   1.528 +                val lhs = #1 (Logic.dest_equals (prop_of (final init)))
   1.529 +            in
   1.530 +                if not (lhs aconv origt)
   1.531 +                then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
   1.532 +                      writeln (string_of_cterm (cterm_of thy origt));
   1.533 +                      writeln (string_of_cterm (cterm_of thy lhs));
   1.534 +                      writeln (string_of_cterm (cterm_of thy typet));
   1.535 +                      writeln (string_of_cterm (cterm_of thy t));
   1.536 +                      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
   1.537 +                      writeln "done")
   1.538 +                else ()
   1.539 +            end
   1.540      in
   1.541 -	case t of
   1.542 -	    Const("==",T) $ P $ Q =>
   1.543 -	    if is_Abs P orelse is_Abs Q
   1.544 -	    then (case domain_type T of
   1.545 -		      Type("fun",[aT,bT]) =>
   1.546 -		      let
   1.547 -			  val cert = cterm_of thy
   1.548 -			  val vname = Name.variant (add_term_free_names(t,[])) "v"
   1.549 -			  val v = Free(vname,aT)
   1.550 -			  val cv = cert v
   1.551 -			  val ct = cert t
   1.552 -			  val th1 = (combination (assume ct) (reflexive cv))
   1.553 -					|> forall_intr cv
   1.554 -					|> implies_intr ct
   1.555 -			  val concl = cert (concl_of th1)
   1.556 -			  val th2 = (assume concl)
   1.557 -					|> forall_elim cv
   1.558 -					|> abstract_rule vname cv
   1.559 -			  val (lhs,rhs) = Logic.dest_equals (prop_of th2)
   1.560 -			  val elhs = eta_conversion (cert lhs)
   1.561 -			  val erhs = eta_conversion (cert rhs)
   1.562 -			  val th2' = transitive
   1.563 -					 (transitive (symmetric elhs) th2)
   1.564 -					 erhs
   1.565 -			  val res = equal_intr th1 (th2' |> implies_intr concl)
   1.566 -			  val res' = final res
   1.567 -		      in
   1.568 -			  SOME res'
   1.569 -		      end
   1.570 -		    | _ => NONE)
   1.571 -	    else NONE
   1.572 -	  | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE)
   1.573 +        case t of
   1.574 +            Const("==",T) $ P $ Q =>
   1.575 +            if is_Abs P orelse is_Abs Q
   1.576 +            then (case domain_type T of
   1.577 +                      Type("fun",[aT,bT]) =>
   1.578 +                      let
   1.579 +                          val cert = cterm_of thy
   1.580 +                          val vname = Name.variant (add_term_free_names(t,[])) "v"
   1.581 +                          val v = Free(vname,aT)
   1.582 +                          val cv = cert v
   1.583 +                          val ct = cert t
   1.584 +                          val th1 = (combination (assume ct) (reflexive cv))
   1.585 +                                        |> forall_intr cv
   1.586 +                                        |> implies_intr ct
   1.587 +                          val concl = cert (concl_of th1)
   1.588 +                          val th2 = (assume concl)
   1.589 +                                        |> forall_elim cv
   1.590 +                                        |> abstract_rule vname cv
   1.591 +                          val (lhs,rhs) = Logic.dest_equals (prop_of th2)
   1.592 +                          val elhs = eta_conversion (cert lhs)
   1.593 +                          val erhs = eta_conversion (cert rhs)
   1.594 +                          val th2' = transitive
   1.595 +                                         (transitive (symmetric elhs) th2)
   1.596 +                                         erhs
   1.597 +                          val res = equal_intr th1 (th2' |> implies_intr concl)
   1.598 +                          val res' = final res
   1.599 +                      in
   1.600 +                          SOME res'
   1.601 +                      end
   1.602 +                    | _ => NONE)
   1.603 +            else NONE
   1.604 +          | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE)
   1.605      end
   1.606      handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
   1.607  
   1.608 @@ -424,32 +424,32 @@
   1.609  val S'  = mk_free "S'" xT
   1.610  in
   1.611  fun beta_simproc thy = Simplifier.simproc_i
   1.612 -		      thy
   1.613 -		      "Beta-contraction"
   1.614 -		      [Abs("x",xT,Q) $ S]
   1.615 -		      beta_fun
   1.616 +                      thy
   1.617 +                      "Beta-contraction"
   1.618 +                      [Abs("x",xT,Q) $ S]
   1.619 +                      beta_fun
   1.620  
   1.621  fun equals_simproc thy = Simplifier.simproc_i
   1.622 -		      thy
   1.623 -		      "Ordered rewriting of meta equalities"
   1.624 -		      [Const("op ==",xT) $ S $ S']
   1.625 -		      equals_fun
   1.626 +                      thy
   1.627 +                      "Ordered rewriting of meta equalities"
   1.628 +                      [Const("op ==",xT) $ S $ S']
   1.629 +                      equals_fun
   1.630  
   1.631  fun quant_simproc thy = Simplifier.simproc_i
   1.632 -			   thy
   1.633 -			   "Ordered rewriting of nested quantifiers"
   1.634 -			   [all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))]
   1.635 -			   quant_rewrite
   1.636 +                           thy
   1.637 +                           "Ordered rewriting of nested quantifiers"
   1.638 +                           [all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))]
   1.639 +                           quant_rewrite
   1.640  fun eta_expand_simproc thy = Simplifier.simproc_i
   1.641 -			 thy
   1.642 -			 "Smart eta-expansion by equivalences"
   1.643 -			 [Logic.mk_equals(Q,R)]
   1.644 -			 eta_expand
   1.645 +                         thy
   1.646 +                         "Smart eta-expansion by equivalences"
   1.647 +                         [Logic.mk_equals(Q,R)]
   1.648 +                         eta_expand
   1.649  fun eta_contract_simproc thy = Simplifier.simproc_i
   1.650 -			 thy
   1.651 -			 "Smart handling of eta-contractions"
   1.652 -			 [all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))]
   1.653 -			 eta_contract
   1.654 +                         thy
   1.655 +                         "Smart handling of eta-contractions"
   1.656 +                         [all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))]
   1.657 +                         eta_contract
   1.658  end
   1.659  
   1.660  (* Disambiguates the names of bound variables in a term, returning t
   1.661 @@ -457,29 +457,29 @@
   1.662  
   1.663  fun disamb_bound thy t =
   1.664      let
   1.665 -	
   1.666 -	fun F (t $ u,idx) =
   1.667 -	    let
   1.668 -		val (t',idx') = F (t,idx)
   1.669 -		val (u',idx'') = F (u,idx')
   1.670 -	    in
   1.671 -		(t' $ u',idx'')
   1.672 -	    end
   1.673 -	  | F (Abs(x,xT,t),idx) =
   1.674 -	    let
   1.675 -		val x' = "x" ^ (LargeInt.toString idx) (* amazing *)
   1.676 -		val (t',idx') = F (t,idx+1)
   1.677 -	    in
   1.678 -		(Abs(x',xT,t'),idx')
   1.679 -	    end
   1.680 -	  | F arg = arg
   1.681 -	val (t',_) = F (t,0)
   1.682 -	val ct = cterm_of thy t
   1.683 -	val ct' = cterm_of thy t'
   1.684 -	val res = transitive (reflexive ct) (reflexive ct')
   1.685 -	val _ = message ("disamb_term: " ^ (string_of_thm res))
   1.686 +
   1.687 +        fun F (t $ u,idx) =
   1.688 +            let
   1.689 +                val (t',idx') = F (t,idx)
   1.690 +                val (u',idx'') = F (u,idx')
   1.691 +            in
   1.692 +                (t' $ u',idx'')
   1.693 +            end
   1.694 +          | F (Abs(x,xT,t),idx) =
   1.695 +            let
   1.696 +                val x' = "x" ^ (LargeInt.toString idx) (* amazing *)
   1.697 +                val (t',idx') = F (t,idx+1)
   1.698 +            in
   1.699 +                (Abs(x',xT,t'),idx')
   1.700 +            end
   1.701 +          | F arg = arg
   1.702 +        val (t',_) = F (t,0)
   1.703 +        val ct = cterm_of thy t
   1.704 +        val ct' = cterm_of thy t'
   1.705 +        val res = transitive (reflexive ct) (reflexive ct')
   1.706 +        val _ = message ("disamb_term: " ^ (string_of_thm res))
   1.707      in
   1.708 -	res
   1.709 +        res
   1.710      end
   1.711  
   1.712  (* Transforms a term t to some normal form t', returning the theorem t
   1.713 @@ -488,25 +488,25 @@
   1.714  
   1.715  fun norm_term thy t =
   1.716      let
   1.717 -	val norms = ShuffleData.get thy
   1.718 -	val ss = Simplifier.theory_context thy empty_ss
   1.719 +        val norms = ShuffleData.get thy
   1.720 +        val ss = Simplifier.theory_context thy empty_ss
   1.721            setmksimps single
   1.722 -	  addsimps (map (Thm.transfer thy) norms)
   1.723 +          addsimps (map (Thm.transfer thy) norms)
   1.724            addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
   1.725 -	fun chain f th =
   1.726 -	    let
   1.727 +        fun chain f th =
   1.728 +            let
   1.729                  val rhs = snd (dest_equals (cprop_of th))
   1.730 -      	    in
   1.731 -		transitive th (f rhs)
   1.732 -	    end
   1.733 -	val th =
   1.734 +            in
   1.735 +                transitive th (f rhs)
   1.736 +            end
   1.737 +        val th =
   1.738              t |> disamb_bound thy
   1.739 -	      |> chain (Simplifier.full_rewrite ss)
   1.740 +              |> chain (Simplifier.full_rewrite ss)
   1.741                |> chain eta_conversion
   1.742 -	      |> strip_shyps
   1.743 -	val _ = message ("norm_term: " ^ (string_of_thm th))
   1.744 +              |> strip_shyps
   1.745 +        val _ = message ("norm_term: " ^ (string_of_thm th))
   1.746      in
   1.747 -	th
   1.748 +        th
   1.749      end
   1.750      handle e => (writeln "norm_term internal error"; print_sign_exn thy e)
   1.751  
   1.752 @@ -516,11 +516,11 @@
   1.753  
   1.754  fun close_thm th =
   1.755      let
   1.756 -	val thy = sign_of_thm th
   1.757 -	val c = prop_of th
   1.758 -	val vars = add_term_frees (c,add_term_vars(c,[]))
   1.759 +        val thy = sign_of_thm th
   1.760 +        val c = prop_of th
   1.761 +        val vars = add_term_frees (c,add_term_vars(c,[]))
   1.762      in
   1.763 -	Drule.forall_intr_list (map (cterm_of thy) vars) th
   1.764 +        Drule.forall_intr_list (map (cterm_of thy) vars) th
   1.765      end
   1.766      handle e => (writeln "close_thm internal error"; OldGoals.print_exn e)
   1.767  
   1.768 @@ -528,9 +528,9 @@
   1.769  
   1.770  fun norm_thm thy th =
   1.771      let
   1.772 -	val c = prop_of th
   1.773 +        val c = prop_of th
   1.774      in
   1.775 -	equal_elim (norm_term thy c) th
   1.776 +        equal_elim (norm_term thy c) th
   1.777      end
   1.778  
   1.779  (* make_equal thy t u tries to construct the theorem t == u under the
   1.780 @@ -539,43 +539,43 @@
   1.781  
   1.782  fun make_equal thy t u =
   1.783      let
   1.784 -	val t_is_t' = norm_term thy t
   1.785 -	val u_is_u' = norm_term thy u
   1.786 -	val th = transitive t_is_t' (symmetric u_is_u')
   1.787 -	val _ = message ("make_equal: SOME " ^ (string_of_thm th))
   1.788 +        val t_is_t' = norm_term thy t
   1.789 +        val u_is_u' = norm_term thy u
   1.790 +        val th = transitive t_is_t' (symmetric u_is_u')
   1.791 +        val _ = message ("make_equal: SOME " ^ (string_of_thm th))
   1.792      in
   1.793 -	SOME th
   1.794 +        SOME th
   1.795      end
   1.796      handle e as THM _ => (message "make_equal: NONE";NONE)
   1.797 -			 
   1.798 +
   1.799  fun match_consts ignore t (* th *) =
   1.800      let
   1.801 -	fun add_consts (Const (c, _), cs) =
   1.802 -	    if c mem_string ignore
   1.803 -	    then cs
   1.804 -	    else insert (op =) c cs
   1.805 -	  | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
   1.806 -	  | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
   1.807 -	  | add_consts (_, cs) = cs
   1.808 -	val t_consts = add_consts(t,[])
   1.809 +        fun add_consts (Const (c, _), cs) =
   1.810 +            if c mem_string ignore
   1.811 +            then cs
   1.812 +            else insert (op =) c cs
   1.813 +          | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
   1.814 +          | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
   1.815 +          | add_consts (_, cs) = cs
   1.816 +        val t_consts = add_consts(t,[])
   1.817      in
   1.818       fn (name,th) =>
   1.819 -	let
   1.820 -	    val th_consts = add_consts(prop_of th,[])
   1.821 -	in
   1.822 -	    eq_set(t_consts,th_consts)
   1.823 -	end
   1.824 +        let
   1.825 +            val th_consts = add_consts(prop_of th,[])
   1.826 +        in
   1.827 +            eq_set(t_consts,th_consts)
   1.828 +        end
   1.829      end
   1.830 -    
   1.831 +
   1.832  val collect_ignored =
   1.833      fold_rev (fn thm => fn cs =>
   1.834 -	      let
   1.835 -		  val (lhs,rhs) = Logic.dest_equals (prop_of thm)
   1.836 -		  val ignore_lhs = term_consts lhs \\ term_consts rhs
   1.837 -		  val ignore_rhs = term_consts rhs \\ term_consts lhs
   1.838 -	      in
   1.839 -		  fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
   1.840 -	      end)
   1.841 +              let
   1.842 +                  val (lhs,rhs) = Logic.dest_equals (prop_of thm)
   1.843 +                  val ignore_lhs = term_consts lhs \\ term_consts rhs
   1.844 +                  val ignore_rhs = term_consts rhs \\ term_consts lhs
   1.845 +              in
   1.846 +                  fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
   1.847 +              end)
   1.848  
   1.849  (* set_prop t thms tries to make a theorem with the proposition t from
   1.850  one of the theorems thms, by shuffling the propositions around.  If it
   1.851 @@ -583,67 +583,67 @@
   1.852  
   1.853  fun set_prop thy t =
   1.854      let
   1.855 -	val vars = add_term_frees (t,add_term_vars (t,[]))
   1.856 -	val closed_t = Library.foldr (fn (v, body) =>
   1.857 +        val vars = add_term_frees (t,add_term_vars (t,[]))
   1.858 +        val closed_t = Library.foldr (fn (v, body) =>
   1.859        let val vT = type_of v in all vT $ (Abs ("x", vT, abstract_over (v, body))) end) (vars, t)
   1.860 -	val rew_th = norm_term thy closed_t
   1.861 -	val rhs = snd (dest_equals (cprop_of rew_th))
   1.862 +        val rew_th = norm_term thy closed_t
   1.863 +        val rhs = snd (dest_equals (cprop_of rew_th))
   1.864  
   1.865 -	val shuffles = ShuffleData.get thy
   1.866 -	fun process [] = NONE
   1.867 -	  | process ((name,th)::thms) =
   1.868 -	    let
   1.869 -		val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
   1.870 -		val triv_th = trivial rhs
   1.871 -		val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
   1.872 -		val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
   1.873 -				 SOME(th,_) => SOME th
   1.874 -			       | NONE => NONE
   1.875 -	    in
   1.876 -		case mod_th of
   1.877 -		    SOME mod_th =>
   1.878 -		    let
   1.879 -			val closed_th = equal_elim (symmetric rew_th) mod_th
   1.880 -		    in
   1.881 -			message ("Shuffler.set_prop succeeded by " ^ name);
   1.882 -			SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th)
   1.883 -		    end
   1.884 -		  | NONE => process thms
   1.885 -	    end
   1.886 -	    handle e as THM _ => process thms
   1.887 +        val shuffles = ShuffleData.get thy
   1.888 +        fun process [] = NONE
   1.889 +          | process ((name,th)::thms) =
   1.890 +            let
   1.891 +                val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
   1.892 +                val triv_th = trivial rhs
   1.893 +                val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
   1.894 +                val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
   1.895 +                                 SOME(th,_) => SOME th
   1.896 +                               | NONE => NONE
   1.897 +            in
   1.898 +                case mod_th of
   1.899 +                    SOME mod_th =>
   1.900 +                    let
   1.901 +                        val closed_th = equal_elim (symmetric rew_th) mod_th
   1.902 +                    in
   1.903 +                        message ("Shuffler.set_prop succeeded by " ^ name);
   1.904 +                        SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th)
   1.905 +                    end
   1.906 +                  | NONE => process thms
   1.907 +            end
   1.908 +            handle e as THM _ => process thms
   1.909      in
   1.910 -	fn thms =>
   1.911 -	   case process thms of
   1.912 -	       res as SOME (name,th) => if (prop_of th) aconv t
   1.913 -					then res
   1.914 -					else error "Internal error in set_prop"
   1.915 -	     | NONE => NONE
   1.916 +        fn thms =>
   1.917 +           case process thms of
   1.918 +               res as SOME (name,th) => if (prop_of th) aconv t
   1.919 +                                        then res
   1.920 +                                        else error "Internal error in set_prop"
   1.921 +             | NONE => NONE
   1.922      end
   1.923      handle e => (writeln "set_prop internal error"; OldGoals.print_exn e)
   1.924  
   1.925  fun find_potential thy t =
   1.926      let
   1.927 -	val shuffles = ShuffleData.get thy
   1.928 -	val ignored = collect_ignored shuffles []
   1.929 -	val rel_consts = term_consts t \\ ignored
   1.930 -	val pot_thms = PureThy.thms_containing_consts thy rel_consts
   1.931 +        val shuffles = ShuffleData.get thy
   1.932 +        val ignored = collect_ignored shuffles []
   1.933 +        val rel_consts = term_consts t \\ ignored
   1.934 +        val pot_thms = PureThy.thms_containing_consts thy rel_consts
   1.935      in
   1.936 -	List.filter (match_consts ignored t) pot_thms
   1.937 +        List.filter (match_consts ignored t) pot_thms
   1.938      end
   1.939  
   1.940  fun gen_shuffle_tac thy search thms i st =
   1.941      let
   1.942 -	val _ = message ("Shuffling " ^ (string_of_thm st))
   1.943 -	val t = List.nth(prems_of st,i-1)
   1.944 -	val set = set_prop thy t
   1.945 -	fun process_tac thms st =
   1.946 -	    case set thms of
   1.947 -		SOME (_,th) => Seq.of_list (compose (th,i,st))
   1.948 -	      | NONE => Seq.empty
   1.949 +        val _ = message ("Shuffling " ^ (string_of_thm st))
   1.950 +        val t = List.nth(prems_of st,i-1)
   1.951 +        val set = set_prop thy t
   1.952 +        fun process_tac thms st =
   1.953 +            case set thms of
   1.954 +                SOME (_,th) => Seq.of_list (compose (th,i,st))
   1.955 +              | NONE => Seq.empty
   1.956      in
   1.957 -	(process_tac thms APPEND (if search
   1.958 -				  then process_tac (find_potential thy t)
   1.959 -				  else no_tac)) st
   1.960 +        (process_tac thms APPEND (if search
   1.961 +                                  then process_tac (find_potential thy t)
   1.962 +                                  else no_tac)) st
   1.963      end
   1.964  
   1.965  fun shuffle_tac thms i st =
   1.966 @@ -654,29 +654,29 @@
   1.967  
   1.968  fun shuffle_meth (thms:thm list) ctxt =
   1.969      let
   1.970 -	val thy = ProofContext.theory_of ctxt
   1.971 +        val thy = ProofContext.theory_of ctxt
   1.972      in
   1.973 -	Method.SIMPLE_METHOD' HEADGOAL (gen_shuffle_tac thy false (map (pair "") thms))
   1.974 +        Method.SIMPLE_METHOD' (gen_shuffle_tac thy false (map (pair "") thms))
   1.975      end
   1.976  
   1.977  fun search_meth ctxt =
   1.978      let
   1.979 -	val thy = ProofContext.theory_of ctxt
   1.980 -	val prems = Assumption.prems_of ctxt
   1.981 +        val thy = ProofContext.theory_of ctxt
   1.982 +        val prems = Assumption.prems_of ctxt
   1.983      in
   1.984 -	Method.SIMPLE_METHOD' HEADGOAL (gen_shuffle_tac thy true (map (pair "premise") prems))
   1.985 +        Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
   1.986      end
   1.987  
   1.988  val print_shuffles = ShuffleData.print
   1.989  
   1.990  fun add_shuffle_rule thm thy =
   1.991      let
   1.992 -	val shuffles = ShuffleData.get thy
   1.993 +        val shuffles = ShuffleData.get thy
   1.994      in
   1.995 -	if exists (curry Thm.eq_thm thm) shuffles
   1.996 -	then (warning ((string_of_thm thm) ^ " already known to the shuffler");
   1.997 -	      thy)
   1.998 -	else ShuffleData.put (thm::shuffles) thy
   1.999 +        if exists (curry Thm.eq_thm thm) shuffles
  1.1000 +        then (warning ((string_of_thm thm) ^ " already known to the shuffler");
  1.1001 +              thy)
  1.1002 +        else ShuffleData.put (thm::shuffles) thy
  1.1003      end
  1.1004  
  1.1005  val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I);