# HG changeset patch
# User wenzelm
# Date 1152356077 -7200
# Node ID f48c4a3a34bc3ac394b37c62453048232c6ff2dd
# Parent  a7964311f1fbb7ce065f57d2ede03495167f2409
Goal.prove: context;

diff -r a7964311f1fb -r f48c4a3a34bc src/HOL/Hoare/hoare.ML
--- a/src/HOL/Hoare/hoare.ML	Sat Jul 08 12:54:36 2006 +0200
+++ b/src/HOL/Hoare/hoare.ML	Sat Jul 08 12:54:37 2006 +0200
@@ -80,7 +80,7 @@
                            Free ("P",varsT --> boolT) $ Bound 0));
                    val impl = implies $ (Mset_incl big_Collect) $ 
                                           (Mset_incl small_Collect);
-   in Goal.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
+   in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
 
 end;
 
diff -r a7964311f1fb -r f48c4a3a34bc src/HOL/Hoare/hoareAbort.ML
--- a/src/HOL/Hoare/hoareAbort.ML	Sat Jul 08 12:54:36 2006 +0200
+++ b/src/HOL/Hoare/hoareAbort.ML	Sat Jul 08 12:54:37 2006 +0200
@@ -81,7 +81,7 @@
                            Free ("P",varsT --> boolT) $ Bound 0));
                    val impl = implies $ (Mset_incl big_Collect) $ 
                                           (Mset_incl small_Collect);
-   in Goal.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
+   in Goal.prove (ProofContext.init (Thm.sign_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
 
 end;
 
diff -r a7964311f1fb -r f48c4a3a34bc src/HOL/Hyperreal/transfer.ML
--- a/src/HOL/Hyperreal/transfer.ML	Sat Jul 08 12:54:36 2006 +0200
+++ b/src/HOL/Hyperreal/transfer.ML	Sat Jul 08 12:54:37 2006 +0200
@@ -71,7 +71,7 @@
       resolve_tac [transfer_start] 1 THEN
       REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
       match_tac [reflexive_thm] 1
-  in Goal.prove thy [] [] (Logic.mk_equals (t,u)) (K tac) end
+  in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end
 
 fun transfer_tac ctxt ths =
     SUBGOAL (fn (t,i) =>
diff -r a7964311f1fb -r f48c4a3a34bc src/HOL/Real/ferrante_rackoff_proof.ML
--- a/src/HOL/Real/ferrante_rackoff_proof.ML	Sat Jul 08 12:54:36 2006 +0200
+++ b/src/HOL/Real/ferrante_rackoff_proof.ML	Sat Jul 08 12:54:37 2006 +0200
@@ -19,39 +19,39 @@
     (* Normalization*)
 
 
-	(* Computation of uset *)
+        (* Computation of uset *)
 fun uset x fm = 
     case fm of
-	Const("op &",_)$p$q => (uset x p) union (uset x q)
+        Const("op &",_)$p$q => (uset x p) union (uset x q)
       | Const("op |",_)$p$q => (uset x p) union (uset x q)
       | Const("Orderings.less",_)$s$t => if s=x then [t] 
-			       else if t = x then [s]
-			       else []
+                               else if t = x then [s]
+                               else []
       | Const("Orderings.less_eq",_)$s$t => if s=x then [t] 
-			       else if t = x then [s]
-			       else []
+                               else if t = x then [s]
+                               else []
       | Const("op =",_)$s$t => if s=x then [t] 
-			       else []
+                               else []
       | Const("Not",_)$ (Const("op =",_)$s$t) => if s=x then [t] 
-						 else []
+                                                 else []
       | _ => [];
 val rsT = Type("set",[rT]);
 fun holrealset [] = Const("{}",rsT)
   | holrealset (x::xs) = Const("insert",[rT,rsT] ---> rsT)$x$(holrealset xs);
-fun prove_bysimp thy ss t = Goal.prove thy [] [] 
-		       (HOLogic.mk_Trueprop t) (fn _ => simp_tac ss 1);
+fun prove_bysimp thy ss t = Goal.prove (ProofContext.init thy) [] [] 
+                       (HOLogic.mk_Trueprop t) (fn _ => simp_tac ss 1);
 
 fun inusetthms sg x fm = 
     let val U = uset x fm
-	val hU = holrealset U
-	fun inC T = Const("op :",[T,Type("set",[T])] ---> HOLogic.boolT);
-	val ss = simpset_of sg
-	fun proveinU t = prove_bysimp sg ss ((inC rT)$t$hU)
-	val uf = prove_bysimp sg ss ((inC rsT)$hU$Const("Finite_Set.Finites",Type("set",[rsT])))
+        val hU = holrealset U
+        fun inC T = Const("op :",[T,Type("set",[T])] ---> HOLogic.boolT);
+        val ss = simpset_of sg
+        fun proveinU t = prove_bysimp sg ss ((inC rT)$t$hU)
+        val uf = prove_bysimp sg ss ((inC rsT)$hU$Const("Finite_Set.Finites",Type("set",[rsT])))
     in (U,cterm_of sg hU,map proveinU U,uf)
     end;
 
-	(* Theorems for minus/plusinfinity *)
+        (* Theorems for minus/plusinfinity *)
 val [minf_lt,minf_gt,minf_le,minf_ge,minf_eq,minf_neq,minf_fm,minf_conj,minf_disj] = thms"minf";
 val [pinf_lt,pinf_gt,pinf_le,pinf_ge,pinf_eq,pinf_neq,pinf_fm,pinf_conj,pinf_disj] = thms"pinf";
     (* Theorems for boundedness from below/above *)
@@ -78,7 +78,7 @@
 
 fun dest2 [] = ([],[])
   | dest2 ((x,y)::xs) = let val (x',y') = dest2 xs 
-			    in (x::x',y::y') end ;
+                            in (x::x',y::y') end ;
 fun myfwd (th1,th2,th3,th4,th5) xs =
     let val (ths1,ths2,ths3,ths4,ths5) = dest5 xs
     in (ths1 MRS th1,ths2 MRS th2,ths3 MRS th3,ths4 MRS th4, ths5 MRS th5)
@@ -91,137 +91,137 @@
 
 fun decomp_mpinf sg x (U,CU,uths) fm = 
     let val cx = cterm_of sg x in
-	(case fm of
-	    Const("op &",_)$p$q => 
-	    ([p,q],myfwd (minf_conj,pinf_conj, nmilbnd_conj, npiubnd_conj,lin_dense_conj))	
-	  | Const("op |",_)$p$q => 
-	    ([p,q],myfwd (minf_disj,pinf_disj, nmilbnd_disj,npiubnd_disj,lin_dense_disj))
-	  | Const("Orderings.less",_)$s$t => 
-	    if s= x then 
-		let val ct = cterm_of sg t
-		    val tinU = nth uths (find_index (fn a => a=t) U)
-		    val mith = instantiate' [] [SOME ct] minf_lt
-		    val pith = instantiate' [] [SOME ct] pinf_lt
-		    val nmilth = tinU RS nmilbnd_lt
-		    val npiuth = tinU RS npiubnd_lt
-		    val lindth = tinU RS lin_dense_lt
-		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
-		end 
-	    else if t = x then 
-		let val ct = cterm_of sg s
-		    val tinU = nth uths (find_index (fn a => a=s) U)
-		    val mith = instantiate' [] [SOME ct] minf_gt
-		    val pith = instantiate' [] [SOME ct] pinf_gt
-		    val nmilth = tinU RS nmilbnd_gt
-		    val npiuth = tinU RS npiubnd_gt
-		    val lindth = tinU RS lin_dense_gt
-		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
-		end 
+        (case fm of
+            Const("op &",_)$p$q => 
+            ([p,q],myfwd (minf_conj,pinf_conj, nmilbnd_conj, npiubnd_conj,lin_dense_conj))      
+          | Const("op |",_)$p$q => 
+            ([p,q],myfwd (minf_disj,pinf_disj, nmilbnd_disj,npiubnd_disj,lin_dense_disj))
+          | Const("Orderings.less",_)$s$t => 
+            if s= x then 
+                let val ct = cterm_of sg t
+                    val tinU = nth uths (find_index (fn a => a=t) U)
+                    val mith = instantiate' [] [SOME ct] minf_lt
+                    val pith = instantiate' [] [SOME ct] pinf_lt
+                    val nmilth = tinU RS nmilbnd_lt
+                    val npiuth = tinU RS npiubnd_lt
+                    val lindth = tinU RS lin_dense_lt
+                in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
+                end 
+            else if t = x then 
+                let val ct = cterm_of sg s
+                    val tinU = nth uths (find_index (fn a => a=s) U)
+                    val mith = instantiate' [] [SOME ct] minf_gt
+                    val pith = instantiate' [] [SOME ct] pinf_gt
+                    val nmilth = tinU RS nmilbnd_gt
+                    val npiuth = tinU RS npiubnd_gt
+                    val lindth = tinU RS lin_dense_gt
+                in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
+                end 
 
-	    else
-		let val cfm = cterm_of sg fm 
-		    val mith = instantiate' [] [SOME cfm] minf_fm
-		    val pith = instantiate' [] [SOME cfm] pinf_fm
-		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
-		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
-		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
-		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
-		end
-	  | Const("Orderings.less_eq",_)$s$t => 
-	    if s= x then 
-		let val ct = cterm_of sg t
-		    val tinU = nth uths (find_index (fn a => a=t) U)
-		    val mith = instantiate' [] [SOME ct] minf_le
-		    val pith = instantiate' [] [SOME ct] pinf_le
-		    val nmilth = tinU RS nmilbnd_le
-		    val npiuth = tinU RS npiubnd_le
-		    val lindth = tinU RS lin_dense_le
-		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
-		end 
-	    else if t = x then 
-		let val ct = cterm_of sg s
-		    val tinU = nth uths (find_index (fn a => a=s) U)
-		    val mith = instantiate' [] [SOME ct] minf_ge
-		    val pith = instantiate' [] [SOME ct] pinf_ge
-		    val nmilth = tinU RS nmilbnd_ge
-		    val npiuth = tinU RS npiubnd_ge
-		    val lindth = tinU RS lin_dense_ge
-		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
-		end 
+            else
+                let val cfm = cterm_of sg fm 
+                    val mith = instantiate' [] [SOME cfm] minf_fm
+                    val pith = instantiate' [] [SOME cfm] pinf_fm
+                    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
+                    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
+                    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
+                in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
+                end
+          | Const("Orderings.less_eq",_)$s$t => 
+            if s= x then 
+                let val ct = cterm_of sg t
+                    val tinU = nth uths (find_index (fn a => a=t) U)
+                    val mith = instantiate' [] [SOME ct] minf_le
+                    val pith = instantiate' [] [SOME ct] pinf_le
+                    val nmilth = tinU RS nmilbnd_le
+                    val npiuth = tinU RS npiubnd_le
+                    val lindth = tinU RS lin_dense_le
+                in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
+                end 
+            else if t = x then 
+                let val ct = cterm_of sg s
+                    val tinU = nth uths (find_index (fn a => a=s) U)
+                    val mith = instantiate' [] [SOME ct] minf_ge
+                    val pith = instantiate' [] [SOME ct] pinf_ge
+                    val nmilth = tinU RS nmilbnd_ge
+                    val npiuth = tinU RS npiubnd_ge
+                    val lindth = tinU RS lin_dense_ge
+                in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
+                end 
 
-	    else
-		let val cfm = cterm_of sg fm 
-		    val mith = instantiate' [] [SOME cfm] minf_fm
-		    val pith = instantiate' [] [SOME cfm] pinf_fm
-		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
-		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
-		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
-		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
-		end
-	  | Const("op =",_)$s$t => 
-	    if s= x then 
-		let val ct = cterm_of sg t
-		    val tinU = nth uths (find_index (fn a => a=t) U)
-		    val mith = instantiate' [] [SOME ct] minf_eq
-		    val pith = instantiate' [] [SOME ct] pinf_eq
-		    val nmilth = tinU RS nmilbnd_eq
-		    val npiuth = tinU RS npiubnd_eq
-		    val lindth = tinU RS lin_dense_eq
-		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
-		end 
-	    else
-		let val cfm = cterm_of sg fm 
-		    val mith = instantiate' [] [SOME cfm] minf_fm
-		    val pith = instantiate' [] [SOME cfm] pinf_fm
-		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
-		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
-		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
-		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
-		end
+            else
+                let val cfm = cterm_of sg fm 
+                    val mith = instantiate' [] [SOME cfm] minf_fm
+                    val pith = instantiate' [] [SOME cfm] pinf_fm
+                    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
+                    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
+                    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
+                in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
+                end
+          | Const("op =",_)$s$t => 
+            if s= x then 
+                let val ct = cterm_of sg t
+                    val tinU = nth uths (find_index (fn a => a=t) U)
+                    val mith = instantiate' [] [SOME ct] minf_eq
+                    val pith = instantiate' [] [SOME ct] pinf_eq
+                    val nmilth = tinU RS nmilbnd_eq
+                    val npiuth = tinU RS npiubnd_eq
+                    val lindth = tinU RS lin_dense_eq
+                in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
+                end 
+            else
+                let val cfm = cterm_of sg fm 
+                    val mith = instantiate' [] [SOME cfm] minf_fm
+                    val pith = instantiate' [] [SOME cfm] pinf_fm
+                    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
+                    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
+                    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
+                in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
+                end
 
-	  | Const("Not",_)$(Const("op =",_)$s$t) => 
-	    if s= x then 
-		let val ct = cterm_of sg t
-		    val tinU = nth uths (find_index (fn a => a=t) U)
-		    val mith = instantiate' [] [SOME ct] minf_neq
-		    val pith = instantiate' [] [SOME ct] pinf_neq
-		    val nmilth = tinU RS nmilbnd_neq
-		    val npiuth = tinU RS npiubnd_neq
-		    val lindth = tinU RS lin_dense_neq
-		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
-		end 
-	    else
-		let val cfm = cterm_of sg fm 
-		    val mith = instantiate' [] [SOME cfm] minf_fm
-		    val pith = instantiate' [] [SOME cfm] pinf_fm
-		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
-		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
-		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
-		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
-		end
-	  | _ => let val cfm = cterm_of sg fm 
-		     val mith = instantiate' [] [SOME cfm] minf_fm
-		     val pith = instantiate' [] [SOME cfm] pinf_fm
-		     val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
-		     val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
-		     val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
-		 in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
-		 end)
+          | Const("Not",_)$(Const("op =",_)$s$t) => 
+            if s= x then 
+                let val ct = cterm_of sg t
+                    val tinU = nth uths (find_index (fn a => a=t) U)
+                    val mith = instantiate' [] [SOME ct] minf_neq
+                    val pith = instantiate' [] [SOME ct] pinf_neq
+                    val nmilth = tinU RS nmilbnd_neq
+                    val npiuth = tinU RS npiubnd_neq
+                    val lindth = tinU RS lin_dense_neq
+                in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
+                end 
+            else
+                let val cfm = cterm_of sg fm 
+                    val mith = instantiate' [] [SOME cfm] minf_fm
+                    val pith = instantiate' [] [SOME cfm] pinf_fm
+                    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
+                    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
+                    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
+                in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
+                end
+          | _ => let val cfm = cterm_of sg fm 
+                     val mith = instantiate' [] [SOME cfm] minf_fm
+                     val pith = instantiate' [] [SOME cfm] pinf_fm
+                     val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
+                     val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
+                     val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
+                 in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
+                 end)
     end;
 
 fun ferrack_eq thy p = 
     case p of
-	Const("Ex",_)$Abs(x1,T,p1) => 
-	let val (xn,fm) = variant_abs(x1,T,p1)
-	    val x = Free(xn,T)
-	    val (u,cu,uths,uf) = inusetthms thy x fm
-	    val (mi,pi,nmi,npi,lind) = divide_and_conquer (decomp_mpinf thy x (u,cu,uths)) fm
-	    val frth = [uf,lind,nmi,npi,mi,pi] MRS fr_eq
-	    val (cTp,ceq) = Thm.dest_comb (cprop_of frth)
-	    val qth = (Simplifier.rewrite (HOL_basic_ss addsimps fr_simps addsimps [refl]) 
-					  (snd (Thm.dest_comb ceq))) RS meta_eq_to_obj_eq
-	in [frth,qth] MRS trans
-	end
+        Const("Ex",_)$Abs(x1,T,p1) => 
+        let val (xn,fm) = variant_abs(x1,T,p1)
+            val x = Free(xn,T)
+            val (u,cu,uths,uf) = inusetthms thy x fm
+            val (mi,pi,nmi,npi,lind) = divide_and_conquer (decomp_mpinf thy x (u,cu,uths)) fm
+            val frth = [uf,lind,nmi,npi,mi,pi] MRS fr_eq
+            val (cTp,ceq) = Thm.dest_comb (cprop_of frth)
+            val qth = (Simplifier.rewrite (HOL_basic_ss addsimps fr_simps addsimps [refl]) 
+                                          (snd (Thm.dest_comb ceq))) RS meta_eq_to_obj_eq
+        in [frth,qth] MRS trans
+        end
       | _ => instantiate' [SOME cbT] [SOME (cterm_of thy p)] refl;
 
 (* Code for normalization of terms and Formulae *)
@@ -248,40 +248,40 @@
 
 fun decomp_cnnf lfnp P = 
     case P of 
-	Const ("op &",_) $ p $q => ([p,q] , FWD qe_conjI )
+        Const ("op &",_) $ p $q => ([p,q] , FWD qe_conjI )
       | Const ("op |",_) $ p $q => ([p,q] , FWD qe_disjI)
       | Const ("Not",_) $ (Const("Not",_) $ p) => ([p], FWD nnf_nn)
       | Const("Not",_) $ (Const(opn,T) $ p $ q) => 
-	if opn = "op |" 
-	then 
-	    (case (p,q) of 
-		 (A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) =>
-		 if r1 = CooperDec.negate r 
-		 then  ([r,HOLogic.Not$s,r1,HOLogic.Not$t],
-			fn [th1_1,th1_2,th2_1,th2_2] => 
-			   [[th1_1,th1_1] MRS qe_conjI,[th2_1,th2_2] MRS qe_conjI] MRS nnf_sdj)
-		       
-		 else ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ndj)
+        if opn = "op |" 
+        then 
+            (case (p,q) of 
+                 (A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) =>
+                 if r1 = CooperDec.negate r 
+                 then  ([r,HOLogic.Not$s,r1,HOLogic.Not$t],
+                        fn [th1_1,th1_2,th2_1,th2_2] => 
+                           [[th1_1,th1_1] MRS qe_conjI,[th2_1,th2_2] MRS qe_conjI] MRS nnf_sdj)
+                       
+                 else ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ndj)
                | (_,_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ndj))
-	else (
+        else (
               case (opn,T) of 
-		  ("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ncj )
-		| ("op -->",_) => ([p,HOLogic.Not $ q ], FWD nnf_nim )
-		| ("op =",Type ("fun",[Type ("bool", []),_])) => 
-		  ([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q], 
-		   FWD nnf_neq)
-		| (_,_) => ([], fn [] => lfnp P))
+                  ("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ncj )
+                | ("op -->",_) => ([p,HOLogic.Not $ q ], FWD nnf_nim )
+                | ("op =",Type ("fun",[Type ("bool", []),_])) => 
+                  ([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q], 
+                   FWD nnf_neq)
+                | (_,_) => ([], fn [] => lfnp P))
       | (Const ("op -->",_) $ p $ q) => ([HOLogic.Not$p,q], FWD nnf_im)
       | (Const ("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q) =>
-	([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], FWD nnf_eq )
+        ([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], FWD nnf_eq )
       | _ => ([], fn [] => lfnp P);
 
 fun nnfp afnp vs p = 
     let val th = divide_and_conquer (decomp_cnnf (afnp vs)) p
-	val Pth = (Simplifier.rewrite 
-		       (HOL_basic_ss addsimps fr_simps addsimps [refl]) 
-		       (snd(Thm.dest_comb(snd(Thm.dest_comb (cprop_of th))))))
-		      RS meta_eq_to_obj_eq
+        val Pth = (Simplifier.rewrite 
+                       (HOL_basic_ss addsimps fr_simps addsimps [refl]) 
+                       (snd(Thm.dest_comb(snd(Thm.dest_comb (cprop_of th))))))
+                      RS meta_eq_to_obj_eq
     in [th,Pth] MRS trans
     end;
 
@@ -291,7 +291,7 @@
 val rone = Const("1",rT);
 fun mk_real i = 
     case i of 
-	0 => rzero
+        0 => rzero
       | 1 => rone
       | _ => (HOLogic.number_of_const rT)$(HOLogic.mk_binum i); 
 
@@ -299,38 +299,38 @@
   | dest_real (Const("1",_)) = 1
   | dest_real (Const("Numeral.number_of",_)$b) = HOLogic.dest_binum b;
 
-	(* Normal form for terms is: 
-	 (c0*x0 + ... + cn*xn + k) / c , where ci!=0 and x0<..<xn ordered according to vs*)
-	(* functions to prove trivial properties about numbers *)
+        (* Normal form for terms is: 
+         (c0*x0 + ... + cn*xn + k) / c , where ci!=0 and x0<..<xn ordered according to vs*)
+        (* functions to prove trivial properties about numbers *)
 fun proveq thy n m = prove_bysimp thy (simpset_of thy) (HOLogic.mk_eq(mk_real n,mk_real m));
 fun provenz thy n = 
     prove_bysimp thy (simpset_of thy) (HOLogic.Not$(HOLogic.mk_eq(mk_real n,rzero)));
 
 fun proveprod thy m n = 
     prove_bysimp thy (simpset_of thy) 
-		 (HOLogic.mk_eq(HOLogic.mk_binop "HOL.times" (mk_real m,mk_real n),mk_real (m*n)));
+                 (HOLogic.mk_eq(HOLogic.mk_binop "HOL.times" (mk_real m,mk_real n),mk_real (m*n)));
 fun proveadd thy m n = 
     prove_bysimp thy (simpset_of thy) 
-		 (HOLogic.mk_eq(HOLogic.mk_binop "HOL.plus" (mk_real m,mk_real n),mk_real (m+n)));
+                 (HOLogic.mk_eq(HOLogic.mk_binop "HOL.plus" (mk_real m,mk_real n),mk_real (m+n)));
 fun provediv thy m n = 
     let val g = gcd (m,n) 
-	val m' = m div g
-	val n'= n div g
+        val m' = m div g
+        val n'= n div g
     in
-	(prove_bysimp thy (simpset_of thy) 
-		     (HOLogic.mk_eq(HOLogic.mk_binop "HOL.divide" (mk_real m,mk_real n),
-				    HOLogic.mk_binop "HOL.divide" 
-						     (mk_real m',mk_real n'))),m')
+        (prove_bysimp thy (simpset_of thy) 
+                     (HOLogic.mk_eq(HOLogic.mk_binop "HOL.divide" (mk_real m,mk_real n),
+                                    HOLogic.mk_binop "HOL.divide" 
+                                                     (mk_real m',mk_real n'))),m')
     end;
-		 (* Multiplication of a normal term by a constant *)
+                 (* Multiplication of a normal term by a constant *)
 val ncmul_congh = thm "ncmul_congh";
 val ncmul_cong = thm "ncmul_cong";
 fun decomp_ncmulh thy c t = 
     if c = 0 then ([],fn _ => instantiate' [SOME crT] [SOME (cterm_of thy t)] mult_zero_left) else 
     case t of 
-	Const("HOL.plus",_)$(Const("HOL.times",_)$c'$v)$b => 
-	([b],FWD (instantiate' [] [NONE, NONE, SOME (cterm_of thy v)] 
-			       ((proveprod thy c (dest_real c')) RS ncmul_congh)))
+        Const("HOL.plus",_)$(Const("HOL.times",_)$c'$v)$b => 
+        ([b],FWD (instantiate' [] [NONE, NONE, SOME (cterm_of thy v)] 
+                               ((proveprod thy c (dest_real c')) RS ncmul_congh)))
       | _ => ([],fn _ => proveprod thy c (dest_real t));
 
 fun prove_ncmulh thy c = divide_and_conquer (decomp_ncmulh thy c);
@@ -338,7 +338,7 @@
     (* prove_ncmul thy n t n = a theorem : "c*(t/n) = (t'/n')*)
 fun prove_ncmul thy c (t,m) = 
     let val (eq1,c') = provediv thy c m
-	val tt' = prove_ncmulh thy c' t
+        val tt' = prove_ncmulh thy c' t
     in [eq1,tt'] MRS ncmul_cong
     end;
 
@@ -360,25 +360,25 @@
 
 fun decomp_naddh thy vs (t,s) = 
     case (t,s) of 
-	(Const("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr, 
-	 Const("HOL.plus",_)$(csv as Const("HOL.times",_)$sc$sv)$sr) =>
-	if tv = sv then 
-	    let val ntc = dest_real tc
-		val nsc = dest_real sc
-		val addth = proveadd thy ntc nsc
-	    in if ntc + nsc = 0 
-	       then ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)] 
-						  (addth RS naddh_cong_same0)))
-	       else ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)] 
-						  (addth RS naddh_cong_same)))
-	    end
-	else if earlier vs tv sv 
-	then ([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
-	else ([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
+        (Const("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr, 
+         Const("HOL.plus",_)$(csv as Const("HOL.times",_)$sc$sv)$sr) =>
+        if tv = sv then 
+            let val ntc = dest_real tc
+                val nsc = dest_real sc
+                val addth = proveadd thy ntc nsc
+            in if ntc + nsc = 0 
+               then ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)] 
+                                                  (addth RS naddh_cong_same0)))
+               else ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)] 
+                                                  (addth RS naddh_cong_same)))
+            end
+        else if earlier vs tv sv 
+        then ([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
+        else ([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
       | (Const("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr,_) => 
-	([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
+        ([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
       | (_,Const("HOL.plus",_)$(csv as Const("HOL.times",_)$sc$sv)$sr) => 
-	([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
+        ([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
       | (_,_) => ([], fn _ => proveadd thy (dest_real t) (dest_real s));
 
     (* prove_naddh returns "t + s = t'*) 
@@ -390,38 +390,38 @@
     (* prove_nadd resturns: "t/m + s/n = t'/m'"*)
 fun prove_nadd thy vs (t,m) (s,n) = 
     if n=m then 
-	let val nm = proveq thy n m
-	    val ts = prove_naddh thy vs (t,s)
-	in [nm,ts] MRS nadd_cong_same
-	end
+        let val nm = proveq thy n m
+            val ts = prove_naddh thy vs (t,s)
+        in [nm,ts] MRS nadd_cong_same
+        end
     else let val l = lcm (m,n)
-	     val m' = l div m
-	     val n' = l div n
-	     val mml = proveprod thy m' m
-	     val nnl = proveprod thy n' n
-	     val mnz = provenz thy m
-	     val nnz = provenz thy n
-	     val lnz = provenz thy l
-	     val mt = prove_ncmulh thy m' t
-	     val ns = prove_ncmulh thy n' s
-	     val _$(_$_$t') = prop_of mt
-	     val _$(_$_$s') = prop_of ns
-	 in [mml,nnl,mnz,nnz,lnz,[mt,ns,prove_naddh thy vs (t',s')] MRS plus_cong] 
-		MRS nadd_cong
-	 end;
+             val m' = l div m
+             val n' = l div n
+             val mml = proveprod thy m' m
+             val nnl = proveprod thy n' n
+             val mnz = provenz thy m
+             val nnz = provenz thy n
+             val lnz = provenz thy l
+             val mt = prove_ncmulh thy m' t
+             val ns = prove_ncmulh thy n' s
+             val _$(_$_$t') = prop_of mt
+             val _$(_$_$s') = prop_of ns
+         in [mml,nnl,mnz,nnz,lnz,[mt,ns,prove_naddh thy vs (t',s')] MRS plus_cong] 
+                MRS nadd_cong
+         end;
 
     (* prove_nsub returns: "t/m - s/n = t'/m'"*)
 val nsub_cong = thm "nsub_cong";
 fun prove_nsub thy vs (t,m) (s,n) = 
     let val nsm = prove_nneg thy (s,n)
-	val _$(_$_$(_$s'$n')) = prop_of nsm
-	val ts = prove_nadd thy vs (t,m) (s',dest_real n')
+        val _$(_$_$(_$s'$n')) = prop_of nsm
+        val ts = prove_nadd thy vs (t,m) (s',dest_real n')
     in [nsm,ts] MRS nsub_cong
     end;
 
 val ndivide_cong = thm "ndivide_cong";
 fun prove_ndivide thy (t,m) n = instantiate' [] [SOME(cterm_of thy t)] 
-					     ((proveprod thy m n) RS ndivide_cong);
+                                             ((proveprod thy m n) RS ndivide_cong);
 
 exception FAILURE of string;
 
@@ -435,67 +435,67 @@
 
 fun decomp_normalizeh thy vs t =
     case t of
-	Free _ => ([], fn _ => instantiate' [] [SOME(cterm_of thy t)] normalizeh_var)
+        Free _ => ([], fn _ => instantiate' [] [SOME(cterm_of thy t)] normalizeh_var)
       | Const("HOL.uminus",_)$a => 
-	([a], 
-	 fn [tha] => let val _$(_$_$(_$a'$n')) = prop_of tha
-			 in [tha,prove_nneg thy (a',dest_real n')] 
-				MRS uminus_cong
-			 end )
+        ([a], 
+         fn [tha] => let val _$(_$_$(_$a'$n')) = prop_of tha
+                         in [tha,prove_nneg thy (a',dest_real n')] 
+                                MRS uminus_cong
+                         end )
       | Const("HOL.plus",_)$a$b => 
-	([a,b], 
-	 fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
-			     val _$(_$_$(_$b'$m')) = prop_of thb
-			 in [tha,thb,prove_nadd thy vs (a',dest_real n') (b',dest_real m')] 
-				MRS plus_cong
-			 end )
+        ([a,b], 
+         fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
+                             val _$(_$_$(_$b'$m')) = prop_of thb
+                         in [tha,thb,prove_nadd thy vs (a',dest_real n') (b',dest_real m')] 
+                                MRS plus_cong
+                         end )
       | Const("HOL.minus",_)$a$b => 
-	([a,b], 
-	 fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
-			     val _$(_$_$(_$b'$m')) = prop_of thb
-			 in [tha,thb,prove_nsub thy vs (a',dest_real n') (b',dest_real m')] 
-				MRS diff_cong
-			 end )
+        ([a,b], 
+         fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
+                             val _$(_$_$(_$b'$m')) = prop_of thb
+                         in [tha,thb,prove_nsub thy vs (a',dest_real n') (b',dest_real m')] 
+                                MRS diff_cong
+                         end )
       | Const("HOL.times",_)$a$b => 
-	if can dest_real a 
-	then ([b], fn [thb] => 
-		      let val _$(_$_$(_$b'$m')) = prop_of thb
-		      in [thb, prove_ncmul thy (dest_real a) (b',dest_real m')] MRS mult_cong
-		      end )
-	else if can dest_real b
-	then ([a], fn [tha] => 
-		      let val _$(_$_$(_$a'$m')) = prop_of tha
-		      in [tha, prove_ncmul thy (dest_real b) (a',dest_real m')] MRS mult_cong2
-		      end )
-	else raise FAILURE "decomp_normalizeh: non linear term"
+        if can dest_real a 
+        then ([b], fn [thb] => 
+                      let val _$(_$_$(_$b'$m')) = prop_of thb
+                      in [thb, prove_ncmul thy (dest_real a) (b',dest_real m')] MRS mult_cong
+                      end )
+        else if can dest_real b
+        then ([a], fn [tha] => 
+                      let val _$(_$_$(_$a'$m')) = prop_of tha
+                      in [tha, prove_ncmul thy (dest_real b) (a',dest_real m')] MRS mult_cong2
+                      end )
+        else raise FAILURE "decomp_normalizeh: non linear term"
       | Const("HOL.divide",_)$a$b => 
-	if can dest_real b
-	then ([a], fn [tha] => 
-		      let val _$(_$_$(_$a'$m')) = prop_of tha
-		      in [tha, prove_ndivide thy (a',dest_real m') (dest_real b)] MRS divide_cong
-		      end )
-	else raise FAILURE "decomp_normalizeh: non linear term"
+        if can dest_real b
+        then ([a], fn [tha] => 
+                      let val _$(_$_$(_$a'$m')) = prop_of tha
+                      in [tha, prove_ndivide thy (a',dest_real m') (dest_real b)] MRS divide_cong
+                      end )
+        else raise FAILURE "decomp_normalizeh: non linear term"
       | _ => ([], fn _ => instantiate' [] [SOME (cterm_of thy t)] nrefl);
 fun prove_normalizeh thy vs = divide_and_conquer (decomp_normalizeh thy vs);
 fun dest_xth vs th = 
     let val _$(_$_$(_$t$n)) = prop_of th
     in (case t of 
-	    Const("HOL.plus",_)$(Const("HOL.times",_)$c$y)$r => 
-	    if vs = [] then (0,t,dest_real n)
-	    else if hd vs = y then (dest_real c, r,dest_real n)
-	    else (0,t,dest_real n)
-	  | _ => (0,t,dest_real n))
+            Const("HOL.plus",_)$(Const("HOL.times",_)$c$y)$r => 
+            if vs = [] then (0,t,dest_real n)
+            else if hd vs = y then (dest_real c, r,dest_real n)
+            else (0,t,dest_real n)
+          | _ => (0,t,dest_real n))
     end;
 
 fun prove_strictsign thy n = 
     prove_bysimp thy (simpset_of thy) 
-		 (HOLogic.mk_binrel "Orderings.less" 
-				    (if n > 0 then (rzero, mk_real n) else (mk_real n, rzero))); 
+                 (HOLogic.mk_binrel "Orderings.less" 
+                                    (if n > 0 then (rzero, mk_real n) else (mk_real n, rzero))); 
 fun prove_fracsign thy (m,n) = 
     let val mn = HOLogic.mk_binop "HOL.divide" (mk_real m, mk_real n)
     in prove_bysimp thy (simpset_of thy) 
-		 (HOLogic.mk_binrel "Orderings.less" 
-				    (if m*n > 0 then (rzero, mn) else (mn, rzero)))
+                 (HOLogic.mk_binrel "Orderings.less" 
+                                    (if m*n > 0 then (rzero, mn) else (mn, rzero)))
     end; 
 
 fun holbool_of true = HOLogic.true_const
@@ -505,15 +505,15 @@
     let fun f s = the (AList.lookup (op =) [("Orderings.less", op <),("Orderings.less_eq", op <=),("op =", op =)] s)
     in 
     prove_bysimp thy (simpset_of thy) (HOLogic.mk_eq
-		 (HOLogic.mk_binrel s 
-				    (HOLogic.mk_binop "HOL.divide" (mk_real m, mk_real n),rzero), 
-				    holbool_of (f s (m*n,0))))
+                 (HOLogic.mk_binrel s 
+                                    (HOLogic.mk_binop "HOL.divide" (mk_real m, mk_real n),rzero), 
+                                    holbool_of (f s (m*n,0))))
     end;
 
 fun proveq_eq thy n m = 
     prove_bysimp thy (simpset_of thy) 
-		 (HOLogic.mk_eq 
-		      (HOLogic.mk_eq(mk_real n, mk_real m),holbool_of (n = m)));
+                 (HOLogic.mk_eq 
+                      (HOLogic.mk_eq(mk_real n, mk_real m),holbool_of (n = m)));
 
 val sum_of_same_denoms = thm "sum_of_same_denoms";
 val sum_of_opposite_denoms = thm "sum_of_opposite_denoms";
@@ -541,71 +541,71 @@
 
 fun prove_normalize thy vs at = 
     case at of 
-	Const("Orderings.less",_)$s$t => 
-	let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
-	    val (cx,r,n) = dest_xth vs smtth
-	in if cx = 0 then if can dest_real r 
-			  then [smtth, prove_fracsign_eq thy "Orderings.less" (dest_real r, n)]
-				   MRS normalize_ltground_cong
-			  else [smtth, prove_strictsign thy n] 
-				   MRS (if n > 0 then normalize_ltnoxpos_cong 
-					else normalize_ltnoxneg_cong)
-	   else let val srn = prove_fracsign thy (n,cx)
-		    val rr' = if cx < 0 
-			      then instantiate' [] [SOME (cterm_of thy r)]
-						((proveadd thy cx (~cx)) RS sum_of_opposite_denoms)
-			      else instantiate' [] [SOME (cterm_of thy (mk_real cx))] 
-						(((prove_ncmulh thy ~1 r) RS nneg_cong) 
-							   RS sum_of_same_denoms)
-		in [smtth,srn,rr'] MRS (if n*cx < 0 then normalize_ltxneg_cong 
-					else normalize_ltxpos_cong)
-		end
-	end
+        Const("Orderings.less",_)$s$t => 
+        let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
+            val (cx,r,n) = dest_xth vs smtth
+        in if cx = 0 then if can dest_real r 
+                          then [smtth, prove_fracsign_eq thy "Orderings.less" (dest_real r, n)]
+                                   MRS normalize_ltground_cong
+                          else [smtth, prove_strictsign thy n] 
+                                   MRS (if n > 0 then normalize_ltnoxpos_cong 
+                                        else normalize_ltnoxneg_cong)
+           else let val srn = prove_fracsign thy (n,cx)
+                    val rr' = if cx < 0 
+                              then instantiate' [] [SOME (cterm_of thy r)]
+                                                ((proveadd thy cx (~cx)) RS sum_of_opposite_denoms)
+                              else instantiate' [] [SOME (cterm_of thy (mk_real cx))] 
+                                                (((prove_ncmulh thy ~1 r) RS nneg_cong) 
+                                                           RS sum_of_same_denoms)
+                in [smtth,srn,rr'] MRS (if n*cx < 0 then normalize_ltxneg_cong 
+                                        else normalize_ltxpos_cong)
+                end
+        end
       | Const("Orderings.less_eq",_)$s$t => 
-	let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
-	    val (cx,r,n) = dest_xth vs smtth
-	in if cx = 0 then if can dest_real r 
-			  then [smtth, prove_fracsign_eq thy "Orderings.less_eq" (dest_real r, n)]
-				   MRS normalize_leground_cong
-			  else [smtth, prove_strictsign thy n] 
-				   MRS (if n > 0 then normalize_lenoxpos_cong 
-					else normalize_lenoxneg_cong)
-	   else let val srn = prove_fracsign thy (n,cx)
-		    val rr' = if cx < 0 
-			      then instantiate' [] [SOME (cterm_of thy r)]
-						((proveadd thy cx (~cx)) RS sum_of_opposite_denoms)
-			      else instantiate' [] [SOME (cterm_of thy (mk_real cx))] 
-						(((prove_ncmulh thy ~1 r) RS nneg_cong) 
-							   RS sum_of_same_denoms)
-		in [smtth,srn,rr'] MRS (if n*cx < 0 then normalize_lexneg_cong 
-					else normalize_lexpos_cong)
-		end
-	end
+        let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
+            val (cx,r,n) = dest_xth vs smtth
+        in if cx = 0 then if can dest_real r 
+                          then [smtth, prove_fracsign_eq thy "Orderings.less_eq" (dest_real r, n)]
+                                   MRS normalize_leground_cong
+                          else [smtth, prove_strictsign thy n] 
+                                   MRS (if n > 0 then normalize_lenoxpos_cong 
+                                        else normalize_lenoxneg_cong)
+           else let val srn = prove_fracsign thy (n,cx)
+                    val rr' = if cx < 0 
+                              then instantiate' [] [SOME (cterm_of thy r)]
+                                                ((proveadd thy cx (~cx)) RS sum_of_opposite_denoms)
+                              else instantiate' [] [SOME (cterm_of thy (mk_real cx))] 
+                                                (((prove_ncmulh thy ~1 r) RS nneg_cong) 
+                                                           RS sum_of_same_denoms)
+                in [smtth,srn,rr'] MRS (if n*cx < 0 then normalize_lexneg_cong 
+                                        else normalize_lexpos_cong)
+                end
+        end
       | Const("op =",_)$s$t => 
-	let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
-	    val (cx,r,n) = dest_xth vs smtth
-	in if cx = 0 then if can dest_real r 
-			  then [smtth, provenz thy n, 
-				proveq_eq thy (dest_real r) 0]
-				   MRS normalize_eqground_cong
-			  else [smtth, provenz thy n] 
-				   MRS normalize_eqnox_cong
-	   else let val scx = prove_strictsign thy cx
-		    val nnz = provenz thy n
-		    val rr' = if cx < 0 
-			      then proveadd thy cx (~cx)
-			      else ((prove_ncmulh thy ~1 r) RS nneg_cong) 
-				       RS trivial_sum_of_opposites
-		in [smtth,scx,nnz,rr'] MRS (if cx < 0 then normalize_eqxneg_cong 
-					else normalize_eqxpos_cong)
-		end
-	end
+        let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
+            val (cx,r,n) = dest_xth vs smtth
+        in if cx = 0 then if can dest_real r 
+                          then [smtth, provenz thy n, 
+                                proveq_eq thy (dest_real r) 0]
+                                   MRS normalize_eqground_cong
+                          else [smtth, provenz thy n] 
+                                   MRS normalize_eqnox_cong
+           else let val scx = prove_strictsign thy cx
+                    val nnz = provenz thy n
+                    val rr' = if cx < 0 
+                              then proveadd thy cx (~cx)
+                              else ((prove_ncmulh thy ~1 r) RS nneg_cong) 
+                                       RS trivial_sum_of_opposites
+                in [smtth,scx,nnz,rr'] MRS (if cx < 0 then normalize_eqxneg_cong 
+                                        else normalize_eqxpos_cong)
+                end
+        end
       | Const("Not",_)$(Const("Orderings.less",T)$s$t) => 
-	(prove_normalize thy vs (Const("Orderings.less_eq",T)$t$s)) RS normalize_not_lt
+        (prove_normalize thy vs (Const("Orderings.less_eq",T)$t$s)) RS normalize_not_lt
       | Const("Not",_)$(Const("Orderings.less_eq",T)$s$t) => 
-	(prove_normalize thy vs (Const("Orderings.less",T)$t$s)) RS normalize_not_le
+        (prove_normalize thy vs (Const("Orderings.less",T)$t$s)) RS normalize_not_le
       | (nt as Const("Not",_))$(Const("op =",T)$s$t) => 
-	(prove_normalize thy vs (Const("op =",T)$s$t)) RS qe_Not
+        (prove_normalize thy vs (Const("op =",T)$s$t)) RS qe_Not
       | _ => instantiate' [SOME cbT] [SOME (cterm_of thy at)] refl;
 
      (* Generic quantifier elimination *)
@@ -618,41 +618,41 @@
 
 fun decomp_genqelim thy afnp nfnp qfnp (P,vs) = 
     case P of
-	(Const("op &",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_conjI)
+        (Const("op &",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_conjI)
       | (Const("op |",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_disjI)
       | (Const("op -->",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_impI)
       | (Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => 
-	([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_eqI)
+        ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_eqI)
       | (Const("Not",_)$p) => ([(p,vs)],fn [th] => th RS qe_Not)
       | (Const("Ex",_)$Abs(xn,xT,p)) => 
-	let val (xn1,p1) = variant_abs(xn,xT,p)
-	    val x= Free(xn1,xT)
-	in ([(p1,x::vs)],
+        let val (xn1,p1) = variant_abs(xn,xT,p)
+            val x= Free(xn1,xT)
+        in ([(p1,x::vs)],
             fn [th1_1] => 
                let val th2 = [th1_1,nfnp (x::vs) (snd (CooperProof.qe_get_terms th1_1))] MRS trans
-		   val eth1 = (forall_intr (cterm_of thy (Free(xn1,xT))) th2) COMP  ex_eq_cong
-		   val th3 = qfnp (snd(CooperProof.qe_get_terms eth1))
+                   val eth1 = (forall_intr (cterm_of thy (Free(xn1,xT))) th2) COMP  ex_eq_cong
+                   val th3 = qfnp (snd(CooperProof.qe_get_terms eth1))
                in [eth1,th3] MRS trans
                end )
-	end
+        end
       | (Const("All",_)$Abs(xn,xT,p)) => 
-	([((HOLogic.exists_const xT)$Abs(xn,xT,HOLogic.Not $ p),vs)], fn [th] => th RS qe_ALL)
+        ([((HOLogic.exists_const xT)$Abs(xn,xT,HOLogic.Not $ p),vs)], fn [th] => th RS qe_ALL)
       | _ => ([], fn [] => afnp vs P);
 
 val fr_prepqelim = thms "fr_prepqelim";
 val prepare_qelim_ss = HOL_basic_ss 
-			   addsimps simp_thms 
-			   addsimps (List.take(ex_simps,4))
-			   addsimps fr_prepqelim
-			   addsimps [not_all,ex_disj_distrib];
+                           addsimps simp_thms 
+                           addsimps (List.take(ex_simps,4))
+                           addsimps fr_prepqelim
+                           addsimps [not_all,ex_disj_distrib];
 
 fun prove_genqelim thy afnp nfnp qfnp P = 
     let val thP = (Simplifier.rewrite prepare_qelim_ss P) RS meta_eq_to_obj_eq
-	val _$(_$_$P') = prop_of thP
-	val vs = term_frees P'
-	val qeth = divide_and_conquer (decomp_genqelim thy afnp nfnp qfnp) (Pattern.eta_long [] P',vs)
-	val _$(_$_$p'') = prop_of qeth
-	val thp' = nfnp vs p''
+        val _$(_$_$P') = prop_of thP
+        val vs = term_frees P'
+        val qeth = divide_and_conquer (decomp_genqelim thy afnp nfnp qfnp) (Pattern.eta_long [] P',vs)
+        val _$(_$_$p'') = prop_of qeth
+        val thp' = nfnp vs p''
     in [[thP, qeth] MRS trans, thp'] MRS trans
     end;
 
@@ -677,17 +677,17 @@
 
 val vs = [Free("x",rT),Free("y",rT),Free("z",rT)] ;
 prove_nsub thy vs
-		    (parser "4*(x::real) + (3*y + 5)" ,54) (parser "3*(y::real) + (4*z + 5)",9);
+                    (parser "4*(x::real) + (3*y + 5)" ,54) (parser "3*(y::real) + (4*z + 5)",9);
 
 prove_ndivide thy (parser "4*(x::real) + (3*y + 5)" ,5) 4;
 prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
-		    (parser "4*(x::real) + 3* ((3*y + 5) + x)");
+                    (parser "4*(x::real) + 3* ((3*y + 5) + x)");
 prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
-		    (parser "4*(x::real) - 3* ((3*y + 5)*9 + x)");
+                    (parser "4*(x::real) - 3* ((3*y + 5)*9 + x)");
 prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
-		    (parser "- x");
+                    (parser "- x");
 prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
-		    (parser "4*(x::real) +3* ((3*y + 5) / 3 - (- x))");
+                    (parser "4*(x::real) +3* ((3*y + 5) / 3 - (- x))");
 
 
 
diff -r a7964311f1fb -r f48c4a3a34bc src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Sat Jul 08 12:54:36 2006 +0200
+++ b/src/HOL/Tools/record_package.ML	Sat Jul 08 12:54:37 2006 +0200
@@ -818,11 +818,12 @@
 
 fun quick_and_dirty_prove stndrd thy asms prop tac =
   if !record_quick_and_dirty_sensitive andalso !quick_and_dirty
-  then Goal.prove thy [] [] (Logic.list_implies (map Logic.varify asms,Logic.varify prop))
+  then Goal.prove (ProofContext.init thy) [] []
+        (Logic.list_implies (map Logic.varify asms,Logic.varify prop))
         (K (SkipProof.cheat_tac HOL.thy))
         (* standard can take quite a while for large records, thats why
          * we varify the proposition manually here.*)
-  else let val prf = Goal.prove thy [] asms prop tac;
+  else let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac;
        in if stndrd then standard prf else prf end;
 
 fun quick_and_dirty_prf noopt opt () =
diff -r a7964311f1fb -r f48c4a3a34bc src/HOLCF/adm_tac.ML
--- a/src/HOLCF/adm_tac.ML	Sat Jul 08 12:54:36 2006 +0200
+++ b/src/HOLCF/adm_tac.ML	Sat Jul 08 12:54:37 2006 +0200
@@ -102,7 +102,7 @@
          | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t));
        val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
        val t' = mk_all params (Logic.list_implies (prems, t));
-       val thm = Goal.prove sign [] [] t' (K (tac 1));
+       val thm = Goal.prove (ProofContext.init sign) [] [] t' (K (tac 1));
   in (ts, thm)::l end
   handle ERROR _ => l;
 
diff -r a7964311f1fb -r f48c4a3a34bc src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Sat Jul 08 12:54:36 2006 +0200
+++ b/src/Provers/quantifier1.ML	Sat Jul 08 12:54:37 2006 +0200
@@ -104,7 +104,8 @@
   in exqu end;
 
 fun prove_conv tac thy tu =
-  Goal.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
+  Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu)
+    (K (rtac iff_reflection 1 THEN tac));
 
 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
 
diff -r a7964311f1fb -r f48c4a3a34bc src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sat Jul 08 12:54:36 2006 +0200
+++ b/src/Pure/Isar/local_defs.ML	Sat Jul 08 12:54:37 2006 +0200
@@ -144,21 +144,19 @@
 
 fun derived_def ctxt conditional prop =
   let
-    val thy = ProofContext.theory_of ctxt;
     val ((c, T), rhs) = prop
-      |> Thm.cterm_of thy
+      |> Thm.cterm_of (ProofContext.theory_of ctxt)
       |> meta_rewrite (Context.Proof ctxt)
       |> (snd o Logic.dest_equals o Thm.prop_of)
       |> K conditional ? Logic.strip_imp_concl
       |> (abs_def o #2 o cert_def ctxt);
     fun prove ctxt' t def =
       let
-        val thy' = ProofContext.theory_of ctxt';
         val prop' = Term.subst_atomic [(Free (c, T), t)] prop;
         val frees = Term.fold_aterms (fn Free (x, _) =>
           if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
       in
-        Goal.prove thy' frees [] prop' (K (ALLGOALS
+        Goal.prove ctxt' frees [] prop' (K (ALLGOALS
           (meta_rewrite_tac ctxt' THEN'
             Tactic.rewrite_goal_tac [def] THEN'
             Tactic.resolve_tac [Drule.reflexive_thm])))
diff -r a7964311f1fb -r f48c4a3a34bc src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Jul 08 12:54:36 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Jul 08 12:54:37 2006 +0200
@@ -716,8 +716,7 @@
 
 fun retrieve_thms _ pick ctxt (Fact s) =
       let
-        val thy = theory_of ctxt;
-        val th = Goal.prove thy [] [] (read_prop ctxt s) (K (ALLGOALS (some_fact_tac ctxt)))
+        val th = Goal.prove ctxt [] [] (read_prop ctxt s) (K (ALLGOALS (some_fact_tac ctxt)))
           handle ERROR msg => cat_error msg "Failed to retrieve literal fact.";
       in pick "" [th] end
   | retrieve_thms from_thy pick ctxt xthmref =
diff -r a7964311f1fb -r f48c4a3a34bc src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Sat Jul 08 12:54:36 2006 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Sat Jul 08 12:54:37 2006 +0200
@@ -9,7 +9,8 @@
 sig
   val make_thm: theory -> term -> thm
   val cheat_tac: theory -> tactic
-  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
+  val prove: ProofContext.context ->
+    string list -> term list -> term -> (thm list -> tactic) -> thm
 end;
 
 structure SkipProof: SKIP_PROOF =
@@ -34,8 +35,8 @@
 fun cheat_tac thy st =
   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
 
-fun prove thy xs asms prop tac =
-  Goal.prove thy xs asms prop
-    (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
+fun prove ctxt xs asms prop tac =
+  Goal.prove ctxt xs asms prop
+    (if ! quick_and_dirty then (K (cheat_tac (ProofContext.theory_of ctxt))) else tac);
 
 end;
diff -r a7964311f1fb -r f48c4a3a34bc src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat Jul 08 12:54:36 2006 +0200
+++ b/src/Pure/axclass.ML	Sat Jul 08 12:54:37 2006 +0200
@@ -233,7 +233,8 @@
 fun prove_classrel raw_rel tac thy =
   let
     val (c1, c2) = cert_classrel thy raw_rel;
-    val th = Goal.prove thy [] [] (Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg =>
+    val th = Goal.prove (ProofContext.init thy) [] []
+        (Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg =>
       cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
         quote (Sign.string_of_classrel thy [c1, c2]));
   in
@@ -246,7 +247,7 @@
   let
     val arity = Sign.cert_arity thy raw_arity;
     val props = Logic.mk_arities arity;
-    val ths = Goal.prove_multi thy [] [] props
+    val ths = Goal.prove_multi (ProofContext.init thy) [] [] props
       (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
         cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
           quote (Sign.string_of_arity thy arity));
diff -r a7964311f1fb -r f48c4a3a34bc src/ZF/Datatype.ML
--- a/src/ZF/Datatype.ML	Sat Jul 08 12:54:36 2006 +0200
+++ b/src/ZF/Datatype.ML	Sat Jul 08 12:54:37 2006 +0200
@@ -87,7 +87,8 @@
                  writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
                else ();
        val goal = Logic.mk_equals (old, new)
-       val thm = Goal.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
+       val thm = Goal.prove (Simplifier.the_context ss) [] [] goal
+         (fn _ => rtac iff_reflection 1 THEN
            simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
          handle ERROR msg =>
          (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);