Goal.prove: context;
authorwenzelm
Sat Jul 08 12:54:37 2006 +0200 (2006-07-08)
changeset 20049f48c4a3a34bc
parent 20048 a7964311f1fb
child 20050 a2fb9d553aad
Goal.prove: context;
src/HOL/Hoare/hoare.ML
src/HOL/Hoare/hoareAbort.ML
src/HOL/Hyperreal/transfer.ML
src/HOL/Real/ferrante_rackoff_proof.ML
src/HOL/Tools/record_package.ML
src/HOLCF/adm_tac.ML
src/Provers/quantifier1.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/skip_proof.ML
src/Pure/axclass.ML
src/ZF/Datatype.ML
     1.1 --- a/src/HOL/Hoare/hoare.ML	Sat Jul 08 12:54:36 2006 +0200
     1.2 +++ b/src/HOL/Hoare/hoare.ML	Sat Jul 08 12:54:37 2006 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4                             Free ("P",varsT --> boolT) $ Bound 0));
     1.5                     val impl = implies $ (Mset_incl big_Collect) $ 
     1.6                                            (Mset_incl small_Collect);
     1.7 -   in Goal.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
     1.8 +   in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
     1.9  
    1.10  end;
    1.11  
     2.1 --- a/src/HOL/Hoare/hoareAbort.ML	Sat Jul 08 12:54:36 2006 +0200
     2.2 +++ b/src/HOL/Hoare/hoareAbort.ML	Sat Jul 08 12:54:37 2006 +0200
     2.3 @@ -81,7 +81,7 @@
     2.4                             Free ("P",varsT --> boolT) $ Bound 0));
     2.5                     val impl = implies $ (Mset_incl big_Collect) $ 
     2.6                                            (Mset_incl small_Collect);
     2.7 -   in Goal.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
     2.8 +   in Goal.prove (ProofContext.init (Thm.sign_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
     2.9  
    2.10  end;
    2.11  
     3.1 --- a/src/HOL/Hyperreal/transfer.ML	Sat Jul 08 12:54:36 2006 +0200
     3.2 +++ b/src/HOL/Hyperreal/transfer.ML	Sat Jul 08 12:54:37 2006 +0200
     3.3 @@ -71,7 +71,7 @@
     3.4        resolve_tac [transfer_start] 1 THEN
     3.5        REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
     3.6        match_tac [reflexive_thm] 1
     3.7 -  in Goal.prove thy [] [] (Logic.mk_equals (t,u)) (K tac) end
     3.8 +  in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end
     3.9  
    3.10  fun transfer_tac ctxt ths =
    3.11      SUBGOAL (fn (t,i) =>
     4.1 --- a/src/HOL/Real/ferrante_rackoff_proof.ML	Sat Jul 08 12:54:36 2006 +0200
     4.2 +++ b/src/HOL/Real/ferrante_rackoff_proof.ML	Sat Jul 08 12:54:37 2006 +0200
     4.3 @@ -19,39 +19,39 @@
     4.4      (* Normalization*)
     4.5  
     4.6  
     4.7 -	(* Computation of uset *)
     4.8 +        (* Computation of uset *)
     4.9  fun uset x fm = 
    4.10      case fm of
    4.11 -	Const("op &",_)$p$q => (uset x p) union (uset x q)
    4.12 +        Const("op &",_)$p$q => (uset x p) union (uset x q)
    4.13        | Const("op |",_)$p$q => (uset x p) union (uset x q)
    4.14        | Const("Orderings.less",_)$s$t => if s=x then [t] 
    4.15 -			       else if t = x then [s]
    4.16 -			       else []
    4.17 +                               else if t = x then [s]
    4.18 +                               else []
    4.19        | Const("Orderings.less_eq",_)$s$t => if s=x then [t] 
    4.20 -			       else if t = x then [s]
    4.21 -			       else []
    4.22 +                               else if t = x then [s]
    4.23 +                               else []
    4.24        | Const("op =",_)$s$t => if s=x then [t] 
    4.25 -			       else []
    4.26 +                               else []
    4.27        | Const("Not",_)$ (Const("op =",_)$s$t) => if s=x then [t] 
    4.28 -						 else []
    4.29 +                                                 else []
    4.30        | _ => [];
    4.31  val rsT = Type("set",[rT]);
    4.32  fun holrealset [] = Const("{}",rsT)
    4.33    | holrealset (x::xs) = Const("insert",[rT,rsT] ---> rsT)$x$(holrealset xs);
    4.34 -fun prove_bysimp thy ss t = Goal.prove thy [] [] 
    4.35 -		       (HOLogic.mk_Trueprop t) (fn _ => simp_tac ss 1);
    4.36 +fun prove_bysimp thy ss t = Goal.prove (ProofContext.init thy) [] [] 
    4.37 +                       (HOLogic.mk_Trueprop t) (fn _ => simp_tac ss 1);
    4.38  
    4.39  fun inusetthms sg x fm = 
    4.40      let val U = uset x fm
    4.41 -	val hU = holrealset U
    4.42 -	fun inC T = Const("op :",[T,Type("set",[T])] ---> HOLogic.boolT);
    4.43 -	val ss = simpset_of sg
    4.44 -	fun proveinU t = prove_bysimp sg ss ((inC rT)$t$hU)
    4.45 -	val uf = prove_bysimp sg ss ((inC rsT)$hU$Const("Finite_Set.Finites",Type("set",[rsT])))
    4.46 +        val hU = holrealset U
    4.47 +        fun inC T = Const("op :",[T,Type("set",[T])] ---> HOLogic.boolT);
    4.48 +        val ss = simpset_of sg
    4.49 +        fun proveinU t = prove_bysimp sg ss ((inC rT)$t$hU)
    4.50 +        val uf = prove_bysimp sg ss ((inC rsT)$hU$Const("Finite_Set.Finites",Type("set",[rsT])))
    4.51      in (U,cterm_of sg hU,map proveinU U,uf)
    4.52      end;
    4.53  
    4.54 -	(* Theorems for minus/plusinfinity *)
    4.55 +        (* Theorems for minus/plusinfinity *)
    4.56  val [minf_lt,minf_gt,minf_le,minf_ge,minf_eq,minf_neq,minf_fm,minf_conj,minf_disj] = thms"minf";
    4.57  val [pinf_lt,pinf_gt,pinf_le,pinf_ge,pinf_eq,pinf_neq,pinf_fm,pinf_conj,pinf_disj] = thms"pinf";
    4.58      (* Theorems for boundedness from below/above *)
    4.59 @@ -78,7 +78,7 @@
    4.60  
    4.61  fun dest2 [] = ([],[])
    4.62    | dest2 ((x,y)::xs) = let val (x',y') = dest2 xs 
    4.63 -			    in (x::x',y::y') end ;
    4.64 +                            in (x::x',y::y') end ;
    4.65  fun myfwd (th1,th2,th3,th4,th5) xs =
    4.66      let val (ths1,ths2,ths3,ths4,ths5) = dest5 xs
    4.67      in (ths1 MRS th1,ths2 MRS th2,ths3 MRS th3,ths4 MRS th4, ths5 MRS th5)
    4.68 @@ -91,137 +91,137 @@
    4.69  
    4.70  fun decomp_mpinf sg x (U,CU,uths) fm = 
    4.71      let val cx = cterm_of sg x in
    4.72 -	(case fm of
    4.73 -	    Const("op &",_)$p$q => 
    4.74 -	    ([p,q],myfwd (minf_conj,pinf_conj, nmilbnd_conj, npiubnd_conj,lin_dense_conj))	
    4.75 -	  | Const("op |",_)$p$q => 
    4.76 -	    ([p,q],myfwd (minf_disj,pinf_disj, nmilbnd_disj,npiubnd_disj,lin_dense_disj))
    4.77 -	  | Const("Orderings.less",_)$s$t => 
    4.78 -	    if s= x then 
    4.79 -		let val ct = cterm_of sg t
    4.80 -		    val tinU = nth uths (find_index (fn a => a=t) U)
    4.81 -		    val mith = instantiate' [] [SOME ct] minf_lt
    4.82 -		    val pith = instantiate' [] [SOME ct] pinf_lt
    4.83 -		    val nmilth = tinU RS nmilbnd_lt
    4.84 -		    val npiuth = tinU RS npiubnd_lt
    4.85 -		    val lindth = tinU RS lin_dense_lt
    4.86 -		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
    4.87 -		end 
    4.88 -	    else if t = x then 
    4.89 -		let val ct = cterm_of sg s
    4.90 -		    val tinU = nth uths (find_index (fn a => a=s) U)
    4.91 -		    val mith = instantiate' [] [SOME ct] minf_gt
    4.92 -		    val pith = instantiate' [] [SOME ct] pinf_gt
    4.93 -		    val nmilth = tinU RS nmilbnd_gt
    4.94 -		    val npiuth = tinU RS npiubnd_gt
    4.95 -		    val lindth = tinU RS lin_dense_gt
    4.96 -		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
    4.97 -		end 
    4.98 +        (case fm of
    4.99 +            Const("op &",_)$p$q => 
   4.100 +            ([p,q],myfwd (minf_conj,pinf_conj, nmilbnd_conj, npiubnd_conj,lin_dense_conj))      
   4.101 +          | Const("op |",_)$p$q => 
   4.102 +            ([p,q],myfwd (minf_disj,pinf_disj, nmilbnd_disj,npiubnd_disj,lin_dense_disj))
   4.103 +          | Const("Orderings.less",_)$s$t => 
   4.104 +            if s= x then 
   4.105 +                let val ct = cterm_of sg t
   4.106 +                    val tinU = nth uths (find_index (fn a => a=t) U)
   4.107 +                    val mith = instantiate' [] [SOME ct] minf_lt
   4.108 +                    val pith = instantiate' [] [SOME ct] pinf_lt
   4.109 +                    val nmilth = tinU RS nmilbnd_lt
   4.110 +                    val npiuth = tinU RS npiubnd_lt
   4.111 +                    val lindth = tinU RS lin_dense_lt
   4.112 +                in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   4.113 +                end 
   4.114 +            else if t = x then 
   4.115 +                let val ct = cterm_of sg s
   4.116 +                    val tinU = nth uths (find_index (fn a => a=s) U)
   4.117 +                    val mith = instantiate' [] [SOME ct] minf_gt
   4.118 +                    val pith = instantiate' [] [SOME ct] pinf_gt
   4.119 +                    val nmilth = tinU RS nmilbnd_gt
   4.120 +                    val npiuth = tinU RS npiubnd_gt
   4.121 +                    val lindth = tinU RS lin_dense_gt
   4.122 +                in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   4.123 +                end 
   4.124  
   4.125 -	    else
   4.126 -		let val cfm = cterm_of sg fm 
   4.127 -		    val mith = instantiate' [] [SOME cfm] minf_fm
   4.128 -		    val pith = instantiate' [] [SOME cfm] pinf_fm
   4.129 -		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
   4.130 -		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
   4.131 -		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
   4.132 -		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
   4.133 -		end
   4.134 -	  | Const("Orderings.less_eq",_)$s$t => 
   4.135 -	    if s= x then 
   4.136 -		let val ct = cterm_of sg t
   4.137 -		    val tinU = nth uths (find_index (fn a => a=t) U)
   4.138 -		    val mith = instantiate' [] [SOME ct] minf_le
   4.139 -		    val pith = instantiate' [] [SOME ct] pinf_le
   4.140 -		    val nmilth = tinU RS nmilbnd_le
   4.141 -		    val npiuth = tinU RS npiubnd_le
   4.142 -		    val lindth = tinU RS lin_dense_le
   4.143 -		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   4.144 -		end 
   4.145 -	    else if t = x then 
   4.146 -		let val ct = cterm_of sg s
   4.147 -		    val tinU = nth uths (find_index (fn a => a=s) U)
   4.148 -		    val mith = instantiate' [] [SOME ct] minf_ge
   4.149 -		    val pith = instantiate' [] [SOME ct] pinf_ge
   4.150 -		    val nmilth = tinU RS nmilbnd_ge
   4.151 -		    val npiuth = tinU RS npiubnd_ge
   4.152 -		    val lindth = tinU RS lin_dense_ge
   4.153 -		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   4.154 -		end 
   4.155 +            else
   4.156 +                let val cfm = cterm_of sg fm 
   4.157 +                    val mith = instantiate' [] [SOME cfm] minf_fm
   4.158 +                    val pith = instantiate' [] [SOME cfm] pinf_fm
   4.159 +                    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
   4.160 +                    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
   4.161 +                    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
   4.162 +                in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
   4.163 +                end
   4.164 +          | Const("Orderings.less_eq",_)$s$t => 
   4.165 +            if s= x then 
   4.166 +                let val ct = cterm_of sg t
   4.167 +                    val tinU = nth uths (find_index (fn a => a=t) U)
   4.168 +                    val mith = instantiate' [] [SOME ct] minf_le
   4.169 +                    val pith = instantiate' [] [SOME ct] pinf_le
   4.170 +                    val nmilth = tinU RS nmilbnd_le
   4.171 +                    val npiuth = tinU RS npiubnd_le
   4.172 +                    val lindth = tinU RS lin_dense_le
   4.173 +                in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   4.174 +                end 
   4.175 +            else if t = x then 
   4.176 +                let val ct = cterm_of sg s
   4.177 +                    val tinU = nth uths (find_index (fn a => a=s) U)
   4.178 +                    val mith = instantiate' [] [SOME ct] minf_ge
   4.179 +                    val pith = instantiate' [] [SOME ct] pinf_ge
   4.180 +                    val nmilth = tinU RS nmilbnd_ge
   4.181 +                    val npiuth = tinU RS npiubnd_ge
   4.182 +                    val lindth = tinU RS lin_dense_ge
   4.183 +                in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   4.184 +                end 
   4.185  
   4.186 -	    else
   4.187 -		let val cfm = cterm_of sg fm 
   4.188 -		    val mith = instantiate' [] [SOME cfm] minf_fm
   4.189 -		    val pith = instantiate' [] [SOME cfm] pinf_fm
   4.190 -		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
   4.191 -		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
   4.192 -		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
   4.193 -		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
   4.194 -		end
   4.195 -	  | Const("op =",_)$s$t => 
   4.196 -	    if s= x then 
   4.197 -		let val ct = cterm_of sg t
   4.198 -		    val tinU = nth uths (find_index (fn a => a=t) U)
   4.199 -		    val mith = instantiate' [] [SOME ct] minf_eq
   4.200 -		    val pith = instantiate' [] [SOME ct] pinf_eq
   4.201 -		    val nmilth = tinU RS nmilbnd_eq
   4.202 -		    val npiuth = tinU RS npiubnd_eq
   4.203 -		    val lindth = tinU RS lin_dense_eq
   4.204 -		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   4.205 -		end 
   4.206 -	    else
   4.207 -		let val cfm = cterm_of sg fm 
   4.208 -		    val mith = instantiate' [] [SOME cfm] minf_fm
   4.209 -		    val pith = instantiate' [] [SOME cfm] pinf_fm
   4.210 -		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
   4.211 -		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
   4.212 -		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
   4.213 -		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
   4.214 -		end
   4.215 +            else
   4.216 +                let val cfm = cterm_of sg fm 
   4.217 +                    val mith = instantiate' [] [SOME cfm] minf_fm
   4.218 +                    val pith = instantiate' [] [SOME cfm] pinf_fm
   4.219 +                    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
   4.220 +                    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
   4.221 +                    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
   4.222 +                in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
   4.223 +                end
   4.224 +          | Const("op =",_)$s$t => 
   4.225 +            if s= x then 
   4.226 +                let val ct = cterm_of sg t
   4.227 +                    val tinU = nth uths (find_index (fn a => a=t) U)
   4.228 +                    val mith = instantiate' [] [SOME ct] minf_eq
   4.229 +                    val pith = instantiate' [] [SOME ct] pinf_eq
   4.230 +                    val nmilth = tinU RS nmilbnd_eq
   4.231 +                    val npiuth = tinU RS npiubnd_eq
   4.232 +                    val lindth = tinU RS lin_dense_eq
   4.233 +                in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   4.234 +                end 
   4.235 +            else
   4.236 +                let val cfm = cterm_of sg fm 
   4.237 +                    val mith = instantiate' [] [SOME cfm] minf_fm
   4.238 +                    val pith = instantiate' [] [SOME cfm] pinf_fm
   4.239 +                    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
   4.240 +                    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
   4.241 +                    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
   4.242 +                in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
   4.243 +                end
   4.244  
   4.245 -	  | Const("Not",_)$(Const("op =",_)$s$t) => 
   4.246 -	    if s= x then 
   4.247 -		let val ct = cterm_of sg t
   4.248 -		    val tinU = nth uths (find_index (fn a => a=t) U)
   4.249 -		    val mith = instantiate' [] [SOME ct] minf_neq
   4.250 -		    val pith = instantiate' [] [SOME ct] pinf_neq
   4.251 -		    val nmilth = tinU RS nmilbnd_neq
   4.252 -		    val npiuth = tinU RS npiubnd_neq
   4.253 -		    val lindth = tinU RS lin_dense_neq
   4.254 -		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   4.255 -		end 
   4.256 -	    else
   4.257 -		let val cfm = cterm_of sg fm 
   4.258 -		    val mith = instantiate' [] [SOME cfm] minf_fm
   4.259 -		    val pith = instantiate' [] [SOME cfm] pinf_fm
   4.260 -		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
   4.261 -		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
   4.262 -		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
   4.263 -		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
   4.264 -		end
   4.265 -	  | _ => let val cfm = cterm_of sg fm 
   4.266 -		     val mith = instantiate' [] [SOME cfm] minf_fm
   4.267 -		     val pith = instantiate' [] [SOME cfm] pinf_fm
   4.268 -		     val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
   4.269 -		     val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
   4.270 -		     val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
   4.271 -		 in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
   4.272 -		 end)
   4.273 +          | Const("Not",_)$(Const("op =",_)$s$t) => 
   4.274 +            if s= x then 
   4.275 +                let val ct = cterm_of sg t
   4.276 +                    val tinU = nth uths (find_index (fn a => a=t) U)
   4.277 +                    val mith = instantiate' [] [SOME ct] minf_neq
   4.278 +                    val pith = instantiate' [] [SOME ct] pinf_neq
   4.279 +                    val nmilth = tinU RS nmilbnd_neq
   4.280 +                    val npiuth = tinU RS npiubnd_neq
   4.281 +                    val lindth = tinU RS lin_dense_neq
   4.282 +                in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   4.283 +                end 
   4.284 +            else
   4.285 +                let val cfm = cterm_of sg fm 
   4.286 +                    val mith = instantiate' [] [SOME cfm] minf_fm
   4.287 +                    val pith = instantiate' [] [SOME cfm] pinf_fm
   4.288 +                    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
   4.289 +                    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
   4.290 +                    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
   4.291 +                in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
   4.292 +                end
   4.293 +          | _ => let val cfm = cterm_of sg fm 
   4.294 +                     val mith = instantiate' [] [SOME cfm] minf_fm
   4.295 +                     val pith = instantiate' [] [SOME cfm] pinf_fm
   4.296 +                     val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
   4.297 +                     val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
   4.298 +                     val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
   4.299 +                 in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
   4.300 +                 end)
   4.301      end;
   4.302  
   4.303  fun ferrack_eq thy p = 
   4.304      case p of
   4.305 -	Const("Ex",_)$Abs(x1,T,p1) => 
   4.306 -	let val (xn,fm) = variant_abs(x1,T,p1)
   4.307 -	    val x = Free(xn,T)
   4.308 -	    val (u,cu,uths,uf) = inusetthms thy x fm
   4.309 -	    val (mi,pi,nmi,npi,lind) = divide_and_conquer (decomp_mpinf thy x (u,cu,uths)) fm
   4.310 -	    val frth = [uf,lind,nmi,npi,mi,pi] MRS fr_eq
   4.311 -	    val (cTp,ceq) = Thm.dest_comb (cprop_of frth)
   4.312 -	    val qth = (Simplifier.rewrite (HOL_basic_ss addsimps fr_simps addsimps [refl]) 
   4.313 -					  (snd (Thm.dest_comb ceq))) RS meta_eq_to_obj_eq
   4.314 -	in [frth,qth] MRS trans
   4.315 -	end
   4.316 +        Const("Ex",_)$Abs(x1,T,p1) => 
   4.317 +        let val (xn,fm) = variant_abs(x1,T,p1)
   4.318 +            val x = Free(xn,T)
   4.319 +            val (u,cu,uths,uf) = inusetthms thy x fm
   4.320 +            val (mi,pi,nmi,npi,lind) = divide_and_conquer (decomp_mpinf thy x (u,cu,uths)) fm
   4.321 +            val frth = [uf,lind,nmi,npi,mi,pi] MRS fr_eq
   4.322 +            val (cTp,ceq) = Thm.dest_comb (cprop_of frth)
   4.323 +            val qth = (Simplifier.rewrite (HOL_basic_ss addsimps fr_simps addsimps [refl]) 
   4.324 +                                          (snd (Thm.dest_comb ceq))) RS meta_eq_to_obj_eq
   4.325 +        in [frth,qth] MRS trans
   4.326 +        end
   4.327        | _ => instantiate' [SOME cbT] [SOME (cterm_of thy p)] refl;
   4.328  
   4.329  (* Code for normalization of terms and Formulae *)
   4.330 @@ -248,40 +248,40 @@
   4.331  
   4.332  fun decomp_cnnf lfnp P = 
   4.333      case P of 
   4.334 -	Const ("op &",_) $ p $q => ([p,q] , FWD qe_conjI )
   4.335 +        Const ("op &",_) $ p $q => ([p,q] , FWD qe_conjI )
   4.336        | Const ("op |",_) $ p $q => ([p,q] , FWD qe_disjI)
   4.337        | Const ("Not",_) $ (Const("Not",_) $ p) => ([p], FWD nnf_nn)
   4.338        | Const("Not",_) $ (Const(opn,T) $ p $ q) => 
   4.339 -	if opn = "op |" 
   4.340 -	then 
   4.341 -	    (case (p,q) of 
   4.342 -		 (A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) =>
   4.343 -		 if r1 = CooperDec.negate r 
   4.344 -		 then  ([r,HOLogic.Not$s,r1,HOLogic.Not$t],
   4.345 -			fn [th1_1,th1_2,th2_1,th2_2] => 
   4.346 -			   [[th1_1,th1_1] MRS qe_conjI,[th2_1,th2_2] MRS qe_conjI] MRS nnf_sdj)
   4.347 -		       
   4.348 -		 else ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ndj)
   4.349 +        if opn = "op |" 
   4.350 +        then 
   4.351 +            (case (p,q) of 
   4.352 +                 (A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) =>
   4.353 +                 if r1 = CooperDec.negate r 
   4.354 +                 then  ([r,HOLogic.Not$s,r1,HOLogic.Not$t],
   4.355 +                        fn [th1_1,th1_2,th2_1,th2_2] => 
   4.356 +                           [[th1_1,th1_1] MRS qe_conjI,[th2_1,th2_2] MRS qe_conjI] MRS nnf_sdj)
   4.357 +                       
   4.358 +                 else ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ndj)
   4.359                 | (_,_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ndj))
   4.360 -	else (
   4.361 +        else (
   4.362                case (opn,T) of 
   4.363 -		  ("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ncj )
   4.364 -		| ("op -->",_) => ([p,HOLogic.Not $ q ], FWD nnf_nim )
   4.365 -		| ("op =",Type ("fun",[Type ("bool", []),_])) => 
   4.366 -		  ([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q], 
   4.367 -		   FWD nnf_neq)
   4.368 -		| (_,_) => ([], fn [] => lfnp P))
   4.369 +                  ("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ncj )
   4.370 +                | ("op -->",_) => ([p,HOLogic.Not $ q ], FWD nnf_nim )
   4.371 +                | ("op =",Type ("fun",[Type ("bool", []),_])) => 
   4.372 +                  ([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q], 
   4.373 +                   FWD nnf_neq)
   4.374 +                | (_,_) => ([], fn [] => lfnp P))
   4.375        | (Const ("op -->",_) $ p $ q) => ([HOLogic.Not$p,q], FWD nnf_im)
   4.376        | (Const ("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q) =>
   4.377 -	([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], FWD nnf_eq )
   4.378 +        ([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], FWD nnf_eq )
   4.379        | _ => ([], fn [] => lfnp P);
   4.380  
   4.381  fun nnfp afnp vs p = 
   4.382      let val th = divide_and_conquer (decomp_cnnf (afnp vs)) p
   4.383 -	val Pth = (Simplifier.rewrite 
   4.384 -		       (HOL_basic_ss addsimps fr_simps addsimps [refl]) 
   4.385 -		       (snd(Thm.dest_comb(snd(Thm.dest_comb (cprop_of th))))))
   4.386 -		      RS meta_eq_to_obj_eq
   4.387 +        val Pth = (Simplifier.rewrite 
   4.388 +                       (HOL_basic_ss addsimps fr_simps addsimps [refl]) 
   4.389 +                       (snd(Thm.dest_comb(snd(Thm.dest_comb (cprop_of th))))))
   4.390 +                      RS meta_eq_to_obj_eq
   4.391      in [th,Pth] MRS trans
   4.392      end;
   4.393  
   4.394 @@ -291,7 +291,7 @@
   4.395  val rone = Const("1",rT);
   4.396  fun mk_real i = 
   4.397      case i of 
   4.398 -	0 => rzero
   4.399 +        0 => rzero
   4.400        | 1 => rone
   4.401        | _ => (HOLogic.number_of_const rT)$(HOLogic.mk_binum i); 
   4.402  
   4.403 @@ -299,38 +299,38 @@
   4.404    | dest_real (Const("1",_)) = 1
   4.405    | dest_real (Const("Numeral.number_of",_)$b) = HOLogic.dest_binum b;
   4.406  
   4.407 -	(* Normal form for terms is: 
   4.408 -	 (c0*x0 + ... + cn*xn + k) / c , where ci!=0 and x0<..<xn ordered according to vs*)
   4.409 -	(* functions to prove trivial properties about numbers *)
   4.410 +        (* Normal form for terms is: 
   4.411 +         (c0*x0 + ... + cn*xn + k) / c , where ci!=0 and x0<..<xn ordered according to vs*)
   4.412 +        (* functions to prove trivial properties about numbers *)
   4.413  fun proveq thy n m = prove_bysimp thy (simpset_of thy) (HOLogic.mk_eq(mk_real n,mk_real m));
   4.414  fun provenz thy n = 
   4.415      prove_bysimp thy (simpset_of thy) (HOLogic.Not$(HOLogic.mk_eq(mk_real n,rzero)));
   4.416  
   4.417  fun proveprod thy m n = 
   4.418      prove_bysimp thy (simpset_of thy) 
   4.419 -		 (HOLogic.mk_eq(HOLogic.mk_binop "HOL.times" (mk_real m,mk_real n),mk_real (m*n)));
   4.420 +                 (HOLogic.mk_eq(HOLogic.mk_binop "HOL.times" (mk_real m,mk_real n),mk_real (m*n)));
   4.421  fun proveadd thy m n = 
   4.422      prove_bysimp thy (simpset_of thy) 
   4.423 -		 (HOLogic.mk_eq(HOLogic.mk_binop "HOL.plus" (mk_real m,mk_real n),mk_real (m+n)));
   4.424 +                 (HOLogic.mk_eq(HOLogic.mk_binop "HOL.plus" (mk_real m,mk_real n),mk_real (m+n)));
   4.425  fun provediv thy m n = 
   4.426      let val g = gcd (m,n) 
   4.427 -	val m' = m div g
   4.428 -	val n'= n div g
   4.429 +        val m' = m div g
   4.430 +        val n'= n div g
   4.431      in
   4.432 -	(prove_bysimp thy (simpset_of thy) 
   4.433 -		     (HOLogic.mk_eq(HOLogic.mk_binop "HOL.divide" (mk_real m,mk_real n),
   4.434 -				    HOLogic.mk_binop "HOL.divide" 
   4.435 -						     (mk_real m',mk_real n'))),m')
   4.436 +        (prove_bysimp thy (simpset_of thy) 
   4.437 +                     (HOLogic.mk_eq(HOLogic.mk_binop "HOL.divide" (mk_real m,mk_real n),
   4.438 +                                    HOLogic.mk_binop "HOL.divide" 
   4.439 +                                                     (mk_real m',mk_real n'))),m')
   4.440      end;
   4.441 -		 (* Multiplication of a normal term by a constant *)
   4.442 +                 (* Multiplication of a normal term by a constant *)
   4.443  val ncmul_congh = thm "ncmul_congh";
   4.444  val ncmul_cong = thm "ncmul_cong";
   4.445  fun decomp_ncmulh thy c t = 
   4.446      if c = 0 then ([],fn _ => instantiate' [SOME crT] [SOME (cterm_of thy t)] mult_zero_left) else 
   4.447      case t of 
   4.448 -	Const("HOL.plus",_)$(Const("HOL.times",_)$c'$v)$b => 
   4.449 -	([b],FWD (instantiate' [] [NONE, NONE, SOME (cterm_of thy v)] 
   4.450 -			       ((proveprod thy c (dest_real c')) RS ncmul_congh)))
   4.451 +        Const("HOL.plus",_)$(Const("HOL.times",_)$c'$v)$b => 
   4.452 +        ([b],FWD (instantiate' [] [NONE, NONE, SOME (cterm_of thy v)] 
   4.453 +                               ((proveprod thy c (dest_real c')) RS ncmul_congh)))
   4.454        | _ => ([],fn _ => proveprod thy c (dest_real t));
   4.455  
   4.456  fun prove_ncmulh thy c = divide_and_conquer (decomp_ncmulh thy c);
   4.457 @@ -338,7 +338,7 @@
   4.458      (* prove_ncmul thy n t n = a theorem : "c*(t/n) = (t'/n')*)
   4.459  fun prove_ncmul thy c (t,m) = 
   4.460      let val (eq1,c') = provediv thy c m
   4.461 -	val tt' = prove_ncmulh thy c' t
   4.462 +        val tt' = prove_ncmulh thy c' t
   4.463      in [eq1,tt'] MRS ncmul_cong
   4.464      end;
   4.465  
   4.466 @@ -360,25 +360,25 @@
   4.467  
   4.468  fun decomp_naddh thy vs (t,s) = 
   4.469      case (t,s) of 
   4.470 -	(Const("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr, 
   4.471 -	 Const("HOL.plus",_)$(csv as Const("HOL.times",_)$sc$sv)$sr) =>
   4.472 -	if tv = sv then 
   4.473 -	    let val ntc = dest_real tc
   4.474 -		val nsc = dest_real sc
   4.475 -		val addth = proveadd thy ntc nsc
   4.476 -	    in if ntc + nsc = 0 
   4.477 -	       then ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)] 
   4.478 -						  (addth RS naddh_cong_same0)))
   4.479 -	       else ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)] 
   4.480 -						  (addth RS naddh_cong_same)))
   4.481 -	    end
   4.482 -	else if earlier vs tv sv 
   4.483 -	then ([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
   4.484 -	else ([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
   4.485 +        (Const("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr, 
   4.486 +         Const("HOL.plus",_)$(csv as Const("HOL.times",_)$sc$sv)$sr) =>
   4.487 +        if tv = sv then 
   4.488 +            let val ntc = dest_real tc
   4.489 +                val nsc = dest_real sc
   4.490 +                val addth = proveadd thy ntc nsc
   4.491 +            in if ntc + nsc = 0 
   4.492 +               then ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)] 
   4.493 +                                                  (addth RS naddh_cong_same0)))
   4.494 +               else ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)] 
   4.495 +                                                  (addth RS naddh_cong_same)))
   4.496 +            end
   4.497 +        else if earlier vs tv sv 
   4.498 +        then ([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
   4.499 +        else ([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
   4.500        | (Const("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr,_) => 
   4.501 -	([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
   4.502 +        ([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
   4.503        | (_,Const("HOL.plus",_)$(csv as Const("HOL.times",_)$sc$sv)$sr) => 
   4.504 -	([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
   4.505 +        ([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
   4.506        | (_,_) => ([], fn _ => proveadd thy (dest_real t) (dest_real s));
   4.507  
   4.508      (* prove_naddh returns "t + s = t'*) 
   4.509 @@ -390,38 +390,38 @@
   4.510      (* prove_nadd resturns: "t/m + s/n = t'/m'"*)
   4.511  fun prove_nadd thy vs (t,m) (s,n) = 
   4.512      if n=m then 
   4.513 -	let val nm = proveq thy n m
   4.514 -	    val ts = prove_naddh thy vs (t,s)
   4.515 -	in [nm,ts] MRS nadd_cong_same
   4.516 -	end
   4.517 +        let val nm = proveq thy n m
   4.518 +            val ts = prove_naddh thy vs (t,s)
   4.519 +        in [nm,ts] MRS nadd_cong_same
   4.520 +        end
   4.521      else let val l = lcm (m,n)
   4.522 -	     val m' = l div m
   4.523 -	     val n' = l div n
   4.524 -	     val mml = proveprod thy m' m
   4.525 -	     val nnl = proveprod thy n' n
   4.526 -	     val mnz = provenz thy m
   4.527 -	     val nnz = provenz thy n
   4.528 -	     val lnz = provenz thy l
   4.529 -	     val mt = prove_ncmulh thy m' t
   4.530 -	     val ns = prove_ncmulh thy n' s
   4.531 -	     val _$(_$_$t') = prop_of mt
   4.532 -	     val _$(_$_$s') = prop_of ns
   4.533 -	 in [mml,nnl,mnz,nnz,lnz,[mt,ns,prove_naddh thy vs (t',s')] MRS plus_cong] 
   4.534 -		MRS nadd_cong
   4.535 -	 end;
   4.536 +             val m' = l div m
   4.537 +             val n' = l div n
   4.538 +             val mml = proveprod thy m' m
   4.539 +             val nnl = proveprod thy n' n
   4.540 +             val mnz = provenz thy m
   4.541 +             val nnz = provenz thy n
   4.542 +             val lnz = provenz thy l
   4.543 +             val mt = prove_ncmulh thy m' t
   4.544 +             val ns = prove_ncmulh thy n' s
   4.545 +             val _$(_$_$t') = prop_of mt
   4.546 +             val _$(_$_$s') = prop_of ns
   4.547 +         in [mml,nnl,mnz,nnz,lnz,[mt,ns,prove_naddh thy vs (t',s')] MRS plus_cong] 
   4.548 +                MRS nadd_cong
   4.549 +         end;
   4.550  
   4.551      (* prove_nsub returns: "t/m - s/n = t'/m'"*)
   4.552  val nsub_cong = thm "nsub_cong";
   4.553  fun prove_nsub thy vs (t,m) (s,n) = 
   4.554      let val nsm = prove_nneg thy (s,n)
   4.555 -	val _$(_$_$(_$s'$n')) = prop_of nsm
   4.556 -	val ts = prove_nadd thy vs (t,m) (s',dest_real n')
   4.557 +        val _$(_$_$(_$s'$n')) = prop_of nsm
   4.558 +        val ts = prove_nadd thy vs (t,m) (s',dest_real n')
   4.559      in [nsm,ts] MRS nsub_cong
   4.560      end;
   4.561  
   4.562  val ndivide_cong = thm "ndivide_cong";
   4.563  fun prove_ndivide thy (t,m) n = instantiate' [] [SOME(cterm_of thy t)] 
   4.564 -					     ((proveprod thy m n) RS ndivide_cong);
   4.565 +                                             ((proveprod thy m n) RS ndivide_cong);
   4.566  
   4.567  exception FAILURE of string;
   4.568  
   4.569 @@ -435,67 +435,67 @@
   4.570  
   4.571  fun decomp_normalizeh thy vs t =
   4.572      case t of
   4.573 -	Free _ => ([], fn _ => instantiate' [] [SOME(cterm_of thy t)] normalizeh_var)
   4.574 +        Free _ => ([], fn _ => instantiate' [] [SOME(cterm_of thy t)] normalizeh_var)
   4.575        | Const("HOL.uminus",_)$a => 
   4.576 -	([a], 
   4.577 -	 fn [tha] => let val _$(_$_$(_$a'$n')) = prop_of tha
   4.578 -			 in [tha,prove_nneg thy (a',dest_real n')] 
   4.579 -				MRS uminus_cong
   4.580 -			 end )
   4.581 +        ([a], 
   4.582 +         fn [tha] => let val _$(_$_$(_$a'$n')) = prop_of tha
   4.583 +                         in [tha,prove_nneg thy (a',dest_real n')] 
   4.584 +                                MRS uminus_cong
   4.585 +                         end )
   4.586        | Const("HOL.plus",_)$a$b => 
   4.587 -	([a,b], 
   4.588 -	 fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
   4.589 -			     val _$(_$_$(_$b'$m')) = prop_of thb
   4.590 -			 in [tha,thb,prove_nadd thy vs (a',dest_real n') (b',dest_real m')] 
   4.591 -				MRS plus_cong
   4.592 -			 end )
   4.593 +        ([a,b], 
   4.594 +         fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
   4.595 +                             val _$(_$_$(_$b'$m')) = prop_of thb
   4.596 +                         in [tha,thb,prove_nadd thy vs (a',dest_real n') (b',dest_real m')] 
   4.597 +                                MRS plus_cong
   4.598 +                         end )
   4.599        | Const("HOL.minus",_)$a$b => 
   4.600 -	([a,b], 
   4.601 -	 fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
   4.602 -			     val _$(_$_$(_$b'$m')) = prop_of thb
   4.603 -			 in [tha,thb,prove_nsub thy vs (a',dest_real n') (b',dest_real m')] 
   4.604 -				MRS diff_cong
   4.605 -			 end )
   4.606 +        ([a,b], 
   4.607 +         fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
   4.608 +                             val _$(_$_$(_$b'$m')) = prop_of thb
   4.609 +                         in [tha,thb,prove_nsub thy vs (a',dest_real n') (b',dest_real m')] 
   4.610 +                                MRS diff_cong
   4.611 +                         end )
   4.612        | Const("HOL.times",_)$a$b => 
   4.613 -	if can dest_real a 
   4.614 -	then ([b], fn [thb] => 
   4.615 -		      let val _$(_$_$(_$b'$m')) = prop_of thb
   4.616 -		      in [thb, prove_ncmul thy (dest_real a) (b',dest_real m')] MRS mult_cong
   4.617 -		      end )
   4.618 -	else if can dest_real b
   4.619 -	then ([a], fn [tha] => 
   4.620 -		      let val _$(_$_$(_$a'$m')) = prop_of tha
   4.621 -		      in [tha, prove_ncmul thy (dest_real b) (a',dest_real m')] MRS mult_cong2
   4.622 -		      end )
   4.623 -	else raise FAILURE "decomp_normalizeh: non linear term"
   4.624 +        if can dest_real a 
   4.625 +        then ([b], fn [thb] => 
   4.626 +                      let val _$(_$_$(_$b'$m')) = prop_of thb
   4.627 +                      in [thb, prove_ncmul thy (dest_real a) (b',dest_real m')] MRS mult_cong
   4.628 +                      end )
   4.629 +        else if can dest_real b
   4.630 +        then ([a], fn [tha] => 
   4.631 +                      let val _$(_$_$(_$a'$m')) = prop_of tha
   4.632 +                      in [tha, prove_ncmul thy (dest_real b) (a',dest_real m')] MRS mult_cong2
   4.633 +                      end )
   4.634 +        else raise FAILURE "decomp_normalizeh: non linear term"
   4.635        | Const("HOL.divide",_)$a$b => 
   4.636 -	if can dest_real b
   4.637 -	then ([a], fn [tha] => 
   4.638 -		      let val _$(_$_$(_$a'$m')) = prop_of tha
   4.639 -		      in [tha, prove_ndivide thy (a',dest_real m') (dest_real b)] MRS divide_cong
   4.640 -		      end )
   4.641 -	else raise FAILURE "decomp_normalizeh: non linear term"
   4.642 +        if can dest_real b
   4.643 +        then ([a], fn [tha] => 
   4.644 +                      let val _$(_$_$(_$a'$m')) = prop_of tha
   4.645 +                      in [tha, prove_ndivide thy (a',dest_real m') (dest_real b)] MRS divide_cong
   4.646 +                      end )
   4.647 +        else raise FAILURE "decomp_normalizeh: non linear term"
   4.648        | _ => ([], fn _ => instantiate' [] [SOME (cterm_of thy t)] nrefl);
   4.649  fun prove_normalizeh thy vs = divide_and_conquer (decomp_normalizeh thy vs);
   4.650  fun dest_xth vs th = 
   4.651      let val _$(_$_$(_$t$n)) = prop_of th
   4.652      in (case t of 
   4.653 -	    Const("HOL.plus",_)$(Const("HOL.times",_)$c$y)$r => 
   4.654 -	    if vs = [] then (0,t,dest_real n)
   4.655 -	    else if hd vs = y then (dest_real c, r,dest_real n)
   4.656 -	    else (0,t,dest_real n)
   4.657 -	  | _ => (0,t,dest_real n))
   4.658 +            Const("HOL.plus",_)$(Const("HOL.times",_)$c$y)$r => 
   4.659 +            if vs = [] then (0,t,dest_real n)
   4.660 +            else if hd vs = y then (dest_real c, r,dest_real n)
   4.661 +            else (0,t,dest_real n)
   4.662 +          | _ => (0,t,dest_real n))
   4.663      end;
   4.664  
   4.665  fun prove_strictsign thy n = 
   4.666      prove_bysimp thy (simpset_of thy) 
   4.667 -		 (HOLogic.mk_binrel "Orderings.less" 
   4.668 -				    (if n > 0 then (rzero, mk_real n) else (mk_real n, rzero))); 
   4.669 +                 (HOLogic.mk_binrel "Orderings.less" 
   4.670 +                                    (if n > 0 then (rzero, mk_real n) else (mk_real n, rzero))); 
   4.671  fun prove_fracsign thy (m,n) = 
   4.672      let val mn = HOLogic.mk_binop "HOL.divide" (mk_real m, mk_real n)
   4.673      in prove_bysimp thy (simpset_of thy) 
   4.674 -		 (HOLogic.mk_binrel "Orderings.less" 
   4.675 -				    (if m*n > 0 then (rzero, mn) else (mn, rzero)))
   4.676 +                 (HOLogic.mk_binrel "Orderings.less" 
   4.677 +                                    (if m*n > 0 then (rzero, mn) else (mn, rzero)))
   4.678      end; 
   4.679  
   4.680  fun holbool_of true = HOLogic.true_const
   4.681 @@ -505,15 +505,15 @@
   4.682      let fun f s = the (AList.lookup (op =) [("Orderings.less", op <),("Orderings.less_eq", op <=),("op =", op =)] s)
   4.683      in 
   4.684      prove_bysimp thy (simpset_of thy) (HOLogic.mk_eq
   4.685 -		 (HOLogic.mk_binrel s 
   4.686 -				    (HOLogic.mk_binop "HOL.divide" (mk_real m, mk_real n),rzero), 
   4.687 -				    holbool_of (f s (m*n,0))))
   4.688 +                 (HOLogic.mk_binrel s 
   4.689 +                                    (HOLogic.mk_binop "HOL.divide" (mk_real m, mk_real n),rzero), 
   4.690 +                                    holbool_of (f s (m*n,0))))
   4.691      end;
   4.692  
   4.693  fun proveq_eq thy n m = 
   4.694      prove_bysimp thy (simpset_of thy) 
   4.695 -		 (HOLogic.mk_eq 
   4.696 -		      (HOLogic.mk_eq(mk_real n, mk_real m),holbool_of (n = m)));
   4.697 +                 (HOLogic.mk_eq 
   4.698 +                      (HOLogic.mk_eq(mk_real n, mk_real m),holbool_of (n = m)));
   4.699  
   4.700  val sum_of_same_denoms = thm "sum_of_same_denoms";
   4.701  val sum_of_opposite_denoms = thm "sum_of_opposite_denoms";
   4.702 @@ -541,71 +541,71 @@
   4.703  
   4.704  fun prove_normalize thy vs at = 
   4.705      case at of 
   4.706 -	Const("Orderings.less",_)$s$t => 
   4.707 -	let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
   4.708 -	    val (cx,r,n) = dest_xth vs smtth
   4.709 -	in if cx = 0 then if can dest_real r 
   4.710 -			  then [smtth, prove_fracsign_eq thy "Orderings.less" (dest_real r, n)]
   4.711 -				   MRS normalize_ltground_cong
   4.712 -			  else [smtth, prove_strictsign thy n] 
   4.713 -				   MRS (if n > 0 then normalize_ltnoxpos_cong 
   4.714 -					else normalize_ltnoxneg_cong)
   4.715 -	   else let val srn = prove_fracsign thy (n,cx)
   4.716 -		    val rr' = if cx < 0 
   4.717 -			      then instantiate' [] [SOME (cterm_of thy r)]
   4.718 -						((proveadd thy cx (~cx)) RS sum_of_opposite_denoms)
   4.719 -			      else instantiate' [] [SOME (cterm_of thy (mk_real cx))] 
   4.720 -						(((prove_ncmulh thy ~1 r) RS nneg_cong) 
   4.721 -							   RS sum_of_same_denoms)
   4.722 -		in [smtth,srn,rr'] MRS (if n*cx < 0 then normalize_ltxneg_cong 
   4.723 -					else normalize_ltxpos_cong)
   4.724 -		end
   4.725 -	end
   4.726 +        Const("Orderings.less",_)$s$t => 
   4.727 +        let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
   4.728 +            val (cx,r,n) = dest_xth vs smtth
   4.729 +        in if cx = 0 then if can dest_real r 
   4.730 +                          then [smtth, prove_fracsign_eq thy "Orderings.less" (dest_real r, n)]
   4.731 +                                   MRS normalize_ltground_cong
   4.732 +                          else [smtth, prove_strictsign thy n] 
   4.733 +                                   MRS (if n > 0 then normalize_ltnoxpos_cong 
   4.734 +                                        else normalize_ltnoxneg_cong)
   4.735 +           else let val srn = prove_fracsign thy (n,cx)
   4.736 +                    val rr' = if cx < 0 
   4.737 +                              then instantiate' [] [SOME (cterm_of thy r)]
   4.738 +                                                ((proveadd thy cx (~cx)) RS sum_of_opposite_denoms)
   4.739 +                              else instantiate' [] [SOME (cterm_of thy (mk_real cx))] 
   4.740 +                                                (((prove_ncmulh thy ~1 r) RS nneg_cong) 
   4.741 +                                                           RS sum_of_same_denoms)
   4.742 +                in [smtth,srn,rr'] MRS (if n*cx < 0 then normalize_ltxneg_cong 
   4.743 +                                        else normalize_ltxpos_cong)
   4.744 +                end
   4.745 +        end
   4.746        | Const("Orderings.less_eq",_)$s$t => 
   4.747 -	let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
   4.748 -	    val (cx,r,n) = dest_xth vs smtth
   4.749 -	in if cx = 0 then if can dest_real r 
   4.750 -			  then [smtth, prove_fracsign_eq thy "Orderings.less_eq" (dest_real r, n)]
   4.751 -				   MRS normalize_leground_cong
   4.752 -			  else [smtth, prove_strictsign thy n] 
   4.753 -				   MRS (if n > 0 then normalize_lenoxpos_cong 
   4.754 -					else normalize_lenoxneg_cong)
   4.755 -	   else let val srn = prove_fracsign thy (n,cx)
   4.756 -		    val rr' = if cx < 0 
   4.757 -			      then instantiate' [] [SOME (cterm_of thy r)]
   4.758 -						((proveadd thy cx (~cx)) RS sum_of_opposite_denoms)
   4.759 -			      else instantiate' [] [SOME (cterm_of thy (mk_real cx))] 
   4.760 -						(((prove_ncmulh thy ~1 r) RS nneg_cong) 
   4.761 -							   RS sum_of_same_denoms)
   4.762 -		in [smtth,srn,rr'] MRS (if n*cx < 0 then normalize_lexneg_cong 
   4.763 -					else normalize_lexpos_cong)
   4.764 -		end
   4.765 -	end
   4.766 +        let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
   4.767 +            val (cx,r,n) = dest_xth vs smtth
   4.768 +        in if cx = 0 then if can dest_real r 
   4.769 +                          then [smtth, prove_fracsign_eq thy "Orderings.less_eq" (dest_real r, n)]
   4.770 +                                   MRS normalize_leground_cong
   4.771 +                          else [smtth, prove_strictsign thy n] 
   4.772 +                                   MRS (if n > 0 then normalize_lenoxpos_cong 
   4.773 +                                        else normalize_lenoxneg_cong)
   4.774 +           else let val srn = prove_fracsign thy (n,cx)
   4.775 +                    val rr' = if cx < 0 
   4.776 +                              then instantiate' [] [SOME (cterm_of thy r)]
   4.777 +                                                ((proveadd thy cx (~cx)) RS sum_of_opposite_denoms)
   4.778 +                              else instantiate' [] [SOME (cterm_of thy (mk_real cx))] 
   4.779 +                                                (((prove_ncmulh thy ~1 r) RS nneg_cong) 
   4.780 +                                                           RS sum_of_same_denoms)
   4.781 +                in [smtth,srn,rr'] MRS (if n*cx < 0 then normalize_lexneg_cong 
   4.782 +                                        else normalize_lexpos_cong)
   4.783 +                end
   4.784 +        end
   4.785        | Const("op =",_)$s$t => 
   4.786 -	let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
   4.787 -	    val (cx,r,n) = dest_xth vs smtth
   4.788 -	in if cx = 0 then if can dest_real r 
   4.789 -			  then [smtth, provenz thy n, 
   4.790 -				proveq_eq thy (dest_real r) 0]
   4.791 -				   MRS normalize_eqground_cong
   4.792 -			  else [smtth, provenz thy n] 
   4.793 -				   MRS normalize_eqnox_cong
   4.794 -	   else let val scx = prove_strictsign thy cx
   4.795 -		    val nnz = provenz thy n
   4.796 -		    val rr' = if cx < 0 
   4.797 -			      then proveadd thy cx (~cx)
   4.798 -			      else ((prove_ncmulh thy ~1 r) RS nneg_cong) 
   4.799 -				       RS trivial_sum_of_opposites
   4.800 -		in [smtth,scx,nnz,rr'] MRS (if cx < 0 then normalize_eqxneg_cong 
   4.801 -					else normalize_eqxpos_cong)
   4.802 -		end
   4.803 -	end
   4.804 +        let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
   4.805 +            val (cx,r,n) = dest_xth vs smtth
   4.806 +        in if cx = 0 then if can dest_real r 
   4.807 +                          then [smtth, provenz thy n, 
   4.808 +                                proveq_eq thy (dest_real r) 0]
   4.809 +                                   MRS normalize_eqground_cong
   4.810 +                          else [smtth, provenz thy n] 
   4.811 +                                   MRS normalize_eqnox_cong
   4.812 +           else let val scx = prove_strictsign thy cx
   4.813 +                    val nnz = provenz thy n
   4.814 +                    val rr' = if cx < 0 
   4.815 +                              then proveadd thy cx (~cx)
   4.816 +                              else ((prove_ncmulh thy ~1 r) RS nneg_cong) 
   4.817 +                                       RS trivial_sum_of_opposites
   4.818 +                in [smtth,scx,nnz,rr'] MRS (if cx < 0 then normalize_eqxneg_cong 
   4.819 +                                        else normalize_eqxpos_cong)
   4.820 +                end
   4.821 +        end
   4.822        | Const("Not",_)$(Const("Orderings.less",T)$s$t) => 
   4.823 -	(prove_normalize thy vs (Const("Orderings.less_eq",T)$t$s)) RS normalize_not_lt
   4.824 +        (prove_normalize thy vs (Const("Orderings.less_eq",T)$t$s)) RS normalize_not_lt
   4.825        | Const("Not",_)$(Const("Orderings.less_eq",T)$s$t) => 
   4.826 -	(prove_normalize thy vs (Const("Orderings.less",T)$t$s)) RS normalize_not_le
   4.827 +        (prove_normalize thy vs (Const("Orderings.less",T)$t$s)) RS normalize_not_le
   4.828        | (nt as Const("Not",_))$(Const("op =",T)$s$t) => 
   4.829 -	(prove_normalize thy vs (Const("op =",T)$s$t)) RS qe_Not
   4.830 +        (prove_normalize thy vs (Const("op =",T)$s$t)) RS qe_Not
   4.831        | _ => instantiate' [SOME cbT] [SOME (cterm_of thy at)] refl;
   4.832  
   4.833       (* Generic quantifier elimination *)
   4.834 @@ -618,41 +618,41 @@
   4.835  
   4.836  fun decomp_genqelim thy afnp nfnp qfnp (P,vs) = 
   4.837      case P of
   4.838 -	(Const("op &",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_conjI)
   4.839 +        (Const("op &",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_conjI)
   4.840        | (Const("op |",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_disjI)
   4.841        | (Const("op -->",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_impI)
   4.842        | (Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => 
   4.843 -	([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_eqI)
   4.844 +        ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_eqI)
   4.845        | (Const("Not",_)$p) => ([(p,vs)],fn [th] => th RS qe_Not)
   4.846        | (Const("Ex",_)$Abs(xn,xT,p)) => 
   4.847 -	let val (xn1,p1) = variant_abs(xn,xT,p)
   4.848 -	    val x= Free(xn1,xT)
   4.849 -	in ([(p1,x::vs)],
   4.850 +        let val (xn1,p1) = variant_abs(xn,xT,p)
   4.851 +            val x= Free(xn1,xT)
   4.852 +        in ([(p1,x::vs)],
   4.853              fn [th1_1] => 
   4.854                 let val th2 = [th1_1,nfnp (x::vs) (snd (CooperProof.qe_get_terms th1_1))] MRS trans
   4.855 -		   val eth1 = (forall_intr (cterm_of thy (Free(xn1,xT))) th2) COMP  ex_eq_cong
   4.856 -		   val th3 = qfnp (snd(CooperProof.qe_get_terms eth1))
   4.857 +                   val eth1 = (forall_intr (cterm_of thy (Free(xn1,xT))) th2) COMP  ex_eq_cong
   4.858 +                   val th3 = qfnp (snd(CooperProof.qe_get_terms eth1))
   4.859                 in [eth1,th3] MRS trans
   4.860                 end )
   4.861 -	end
   4.862 +        end
   4.863        | (Const("All",_)$Abs(xn,xT,p)) => 
   4.864 -	([((HOLogic.exists_const xT)$Abs(xn,xT,HOLogic.Not $ p),vs)], fn [th] => th RS qe_ALL)
   4.865 +        ([((HOLogic.exists_const xT)$Abs(xn,xT,HOLogic.Not $ p),vs)], fn [th] => th RS qe_ALL)
   4.866        | _ => ([], fn [] => afnp vs P);
   4.867  
   4.868  val fr_prepqelim = thms "fr_prepqelim";
   4.869  val prepare_qelim_ss = HOL_basic_ss 
   4.870 -			   addsimps simp_thms 
   4.871 -			   addsimps (List.take(ex_simps,4))
   4.872 -			   addsimps fr_prepqelim
   4.873 -			   addsimps [not_all,ex_disj_distrib];
   4.874 +                           addsimps simp_thms 
   4.875 +                           addsimps (List.take(ex_simps,4))
   4.876 +                           addsimps fr_prepqelim
   4.877 +                           addsimps [not_all,ex_disj_distrib];
   4.878  
   4.879  fun prove_genqelim thy afnp nfnp qfnp P = 
   4.880      let val thP = (Simplifier.rewrite prepare_qelim_ss P) RS meta_eq_to_obj_eq
   4.881 -	val _$(_$_$P') = prop_of thP
   4.882 -	val vs = term_frees P'
   4.883 -	val qeth = divide_and_conquer (decomp_genqelim thy afnp nfnp qfnp) (Pattern.eta_long [] P',vs)
   4.884 -	val _$(_$_$p'') = prop_of qeth
   4.885 -	val thp' = nfnp vs p''
   4.886 +        val _$(_$_$P') = prop_of thP
   4.887 +        val vs = term_frees P'
   4.888 +        val qeth = divide_and_conquer (decomp_genqelim thy afnp nfnp qfnp) (Pattern.eta_long [] P',vs)
   4.889 +        val _$(_$_$p'') = prop_of qeth
   4.890 +        val thp' = nfnp vs p''
   4.891      in [[thP, qeth] MRS trans, thp'] MRS trans
   4.892      end;
   4.893  
   4.894 @@ -677,17 +677,17 @@
   4.895  
   4.896  val vs = [Free("x",rT),Free("y",rT),Free("z",rT)] ;
   4.897  prove_nsub thy vs
   4.898 -		    (parser "4*(x::real) + (3*y + 5)" ,54) (parser "3*(y::real) + (4*z + 5)",9);
   4.899 +                    (parser "4*(x::real) + (3*y + 5)" ,54) (parser "3*(y::real) + (4*z + 5)",9);
   4.900  
   4.901  prove_ndivide thy (parser "4*(x::real) + (3*y + 5)" ,5) 4;
   4.902  prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
   4.903 -		    (parser "4*(x::real) + 3* ((3*y + 5) + x)");
   4.904 +                    (parser "4*(x::real) + 3* ((3*y + 5) + x)");
   4.905  prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
   4.906 -		    (parser "4*(x::real) - 3* ((3*y + 5)*9 + x)");
   4.907 +                    (parser "4*(x::real) - 3* ((3*y + 5)*9 + x)");
   4.908  prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
   4.909 -		    (parser "- x");
   4.910 +                    (parser "- x");
   4.911  prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
   4.912 -		    (parser "4*(x::real) +3* ((3*y + 5) / 3 - (- x))");
   4.913 +                    (parser "4*(x::real) +3* ((3*y + 5) / 3 - (- x))");
   4.914  
   4.915  
   4.916  
     5.1 --- a/src/HOL/Tools/record_package.ML	Sat Jul 08 12:54:36 2006 +0200
     5.2 +++ b/src/HOL/Tools/record_package.ML	Sat Jul 08 12:54:37 2006 +0200
     5.3 @@ -818,11 +818,12 @@
     5.4  
     5.5  fun quick_and_dirty_prove stndrd thy asms prop tac =
     5.6    if !record_quick_and_dirty_sensitive andalso !quick_and_dirty
     5.7 -  then Goal.prove thy [] [] (Logic.list_implies (map Logic.varify asms,Logic.varify prop))
     5.8 +  then Goal.prove (ProofContext.init thy) [] []
     5.9 +        (Logic.list_implies (map Logic.varify asms,Logic.varify prop))
    5.10          (K (SkipProof.cheat_tac HOL.thy))
    5.11          (* standard can take quite a while for large records, thats why
    5.12           * we varify the proposition manually here.*)
    5.13 -  else let val prf = Goal.prove thy [] asms prop tac;
    5.14 +  else let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac;
    5.15         in if stndrd then standard prf else prf end;
    5.16  
    5.17  fun quick_and_dirty_prf noopt opt () =
     6.1 --- a/src/HOLCF/adm_tac.ML	Sat Jul 08 12:54:36 2006 +0200
     6.2 +++ b/src/HOLCF/adm_tac.ML	Sat Jul 08 12:54:37 2006 +0200
     6.3 @@ -102,7 +102,7 @@
     6.4           | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t));
     6.5         val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
     6.6         val t' = mk_all params (Logic.list_implies (prems, t));
     6.7 -       val thm = Goal.prove sign [] [] t' (K (tac 1));
     6.8 +       val thm = Goal.prove (ProofContext.init sign) [] [] t' (K (tac 1));
     6.9    in (ts, thm)::l end
    6.10    handle ERROR _ => l;
    6.11  
     7.1 --- a/src/Provers/quantifier1.ML	Sat Jul 08 12:54:36 2006 +0200
     7.2 +++ b/src/Provers/quantifier1.ML	Sat Jul 08 12:54:37 2006 +0200
     7.3 @@ -104,7 +104,8 @@
     7.4    in exqu end;
     7.5  
     7.6  fun prove_conv tac thy tu =
     7.7 -  Goal.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
     7.8 +  Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu)
     7.9 +    (K (rtac iff_reflection 1 THEN tac));
    7.10  
    7.11  fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
    7.12  
     8.1 --- a/src/Pure/Isar/local_defs.ML	Sat Jul 08 12:54:36 2006 +0200
     8.2 +++ b/src/Pure/Isar/local_defs.ML	Sat Jul 08 12:54:37 2006 +0200
     8.3 @@ -144,21 +144,19 @@
     8.4  
     8.5  fun derived_def ctxt conditional prop =
     8.6    let
     8.7 -    val thy = ProofContext.theory_of ctxt;
     8.8      val ((c, T), rhs) = prop
     8.9 -      |> Thm.cterm_of thy
    8.10 +      |> Thm.cterm_of (ProofContext.theory_of ctxt)
    8.11        |> meta_rewrite (Context.Proof ctxt)
    8.12        |> (snd o Logic.dest_equals o Thm.prop_of)
    8.13        |> K conditional ? Logic.strip_imp_concl
    8.14        |> (abs_def o #2 o cert_def ctxt);
    8.15      fun prove ctxt' t def =
    8.16        let
    8.17 -        val thy' = ProofContext.theory_of ctxt';
    8.18          val prop' = Term.subst_atomic [(Free (c, T), t)] prop;
    8.19          val frees = Term.fold_aterms (fn Free (x, _) =>
    8.20            if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
    8.21        in
    8.22 -        Goal.prove thy' frees [] prop' (K (ALLGOALS
    8.23 +        Goal.prove ctxt' frees [] prop' (K (ALLGOALS
    8.24            (meta_rewrite_tac ctxt' THEN'
    8.25              Tactic.rewrite_goal_tac [def] THEN'
    8.26              Tactic.resolve_tac [Drule.reflexive_thm])))
     9.1 --- a/src/Pure/Isar/proof_context.ML	Sat Jul 08 12:54:36 2006 +0200
     9.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Jul 08 12:54:37 2006 +0200
     9.3 @@ -716,8 +716,7 @@
     9.4  
     9.5  fun retrieve_thms _ pick ctxt (Fact s) =
     9.6        let
     9.7 -        val thy = theory_of ctxt;
     9.8 -        val th = Goal.prove thy [] [] (read_prop ctxt s) (K (ALLGOALS (some_fact_tac ctxt)))
     9.9 +        val th = Goal.prove ctxt [] [] (read_prop ctxt s) (K (ALLGOALS (some_fact_tac ctxt)))
    9.10            handle ERROR msg => cat_error msg "Failed to retrieve literal fact.";
    9.11        in pick "" [th] end
    9.12    | retrieve_thms from_thy pick ctxt xthmref =
    10.1 --- a/src/Pure/Isar/skip_proof.ML	Sat Jul 08 12:54:36 2006 +0200
    10.2 +++ b/src/Pure/Isar/skip_proof.ML	Sat Jul 08 12:54:37 2006 +0200
    10.3 @@ -9,7 +9,8 @@
    10.4  sig
    10.5    val make_thm: theory -> term -> thm
    10.6    val cheat_tac: theory -> tactic
    10.7 -  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    10.8 +  val prove: ProofContext.context ->
    10.9 +    string list -> term list -> term -> (thm list -> tactic) -> thm
   10.10  end;
   10.11  
   10.12  structure SkipProof: SKIP_PROOF =
   10.13 @@ -34,8 +35,8 @@
   10.14  fun cheat_tac thy st =
   10.15    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
   10.16  
   10.17 -fun prove thy xs asms prop tac =
   10.18 -  Goal.prove thy xs asms prop
   10.19 -    (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
   10.20 +fun prove ctxt xs asms prop tac =
   10.21 +  Goal.prove ctxt xs asms prop
   10.22 +    (if ! quick_and_dirty then (K (cheat_tac (ProofContext.theory_of ctxt))) else tac);
   10.23  
   10.24  end;
    11.1 --- a/src/Pure/axclass.ML	Sat Jul 08 12:54:36 2006 +0200
    11.2 +++ b/src/Pure/axclass.ML	Sat Jul 08 12:54:37 2006 +0200
    11.3 @@ -233,7 +233,8 @@
    11.4  fun prove_classrel raw_rel tac thy =
    11.5    let
    11.6      val (c1, c2) = cert_classrel thy raw_rel;
    11.7 -    val th = Goal.prove thy [] [] (Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg =>
    11.8 +    val th = Goal.prove (ProofContext.init thy) [] []
    11.9 +        (Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg =>
   11.10        cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
   11.11          quote (Sign.string_of_classrel thy [c1, c2]));
   11.12    in
   11.13 @@ -246,7 +247,7 @@
   11.14    let
   11.15      val arity = Sign.cert_arity thy raw_arity;
   11.16      val props = Logic.mk_arities arity;
   11.17 -    val ths = Goal.prove_multi thy [] [] props
   11.18 +    val ths = Goal.prove_multi (ProofContext.init thy) [] [] props
   11.19        (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
   11.20          cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
   11.21            quote (Sign.string_of_arity thy arity));
    12.1 --- a/src/ZF/Datatype.ML	Sat Jul 08 12:54:36 2006 +0200
    12.2 +++ b/src/ZF/Datatype.ML	Sat Jul 08 12:54:37 2006 +0200
    12.3 @@ -87,7 +87,8 @@
    12.4                   writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
    12.5                 else ();
    12.6         val goal = Logic.mk_equals (old, new)
    12.7 -       val thm = Goal.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
    12.8 +       val thm = Goal.prove (Simplifier.the_context ss) [] [] goal
    12.9 +         (fn _ => rtac iff_reflection 1 THEN
   12.10             simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
   12.11           handle ERROR msg =>
   12.12           (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);