# HG changeset patch
# User wenzelm
# Date 1273953005 -7200
# Node ID 9bec62c1071483976bed82f9610c891c6b198cc0
# Parent  dbf831a50e4a02d761d8e6ee4fada49b50d7af37
less pervasive names from structure Thm;

diff -r dbf831a50e4a -r 9bec62c10714 src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/FOLP/simp.ML	Sat May 15 21:50:05 2010 +0200
@@ -431,7 +431,7 @@
       are represented by rules, generalized over their parameters*)
 fun add_asms(ss,thm,a,anet,ats,cs) =
     let val As = strip_varify(nth_subgoal i thm, a, []);
-        val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
+        val thms = map (Thm.trivial o cterm_of(Thm.theory_of_thm thm)) As;
         val new_rws = maps mk_rew_rules thms;
         val rwrls = map mk_trans (maps mk_rew_rules thms);
         val anet' = fold_rev lhs_insert_thm rwrls anet;
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sat May 15 21:50:05 2010 +0200
@@ -681,7 +681,7 @@
      else ("Nox",[])
 | t => if t aconv term_of x then ("x",[]) else ("Nox",[]);
 
-fun xnormalize_conv ctxt [] ct = reflexive ct
+fun xnormalize_conv ctxt [] ct = Thm.reflexive ct
 | xnormalize_conv ctxt (vs as (x::_)) ct =
    case term_of ct of
    Const(@{const_name Orderings.less},_)$_$Const(@{const_name Groups.zero},_) =>
@@ -696,8 +696,8 @@
                (Thm.capply @{cterm "Trueprop"}
                   (if neg then Thm.capply (Thm.capply clt c) cz
                     else Thm.capply (Thm.capply clt cz) c))
-        val cth = equal_elim (symmetric cthp) TrueI
-        val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t])
+        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
+        val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t])
              (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
         val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
                    (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
@@ -719,12 +719,12 @@
                (Thm.capply @{cterm "Trueprop"}
                   (if neg then Thm.capply (Thm.capply clt c) cz
                     else Thm.capply (Thm.capply clt cz) c))
-        val cth = equal_elim (symmetric cthp) TrueI
-        val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
+        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
+        val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
              (if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth
         val rth = th
       in rth end
-    | _ => reflexive ct)
+    | _ => Thm.reflexive ct)
 
 
 |  Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Groups.zero},_) =>
@@ -740,8 +740,8 @@
                (Thm.capply @{cterm "Trueprop"}
                   (if neg then Thm.capply (Thm.capply clt c) cz
                     else Thm.capply (Thm.capply clt cz) c))
-        val cth = equal_elim (symmetric cthp) TrueI
-        val th = implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
+        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
+        val th = Thm.implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
              (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
         val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
                    (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
@@ -764,12 +764,12 @@
                (Thm.capply @{cterm "Trueprop"}
                   (if neg then Thm.capply (Thm.capply clt c) cz
                     else Thm.capply (Thm.capply clt cz) c))
-        val cth = equal_elim (symmetric cthp) TrueI
-        val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
+        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
+        val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
              (if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth
         val rth = th
       in rth end
-    | _ => reflexive ct)
+    | _ => Thm.reflexive ct)
 
 |  Const("op =",_)$_$Const(@{const_name Groups.zero},_) =>
    (case whatis x (Thm.dest_arg1 ct) of
@@ -782,8 +782,8 @@
         val cthp = Simplifier.rewrite (simpset_of ctxt)
             (Thm.capply @{cterm "Trueprop"}
              (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
-        val cth = equal_elim (symmetric cthp) TrueI
-        val th = implies_elim
+        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
+        val th = Thm.implies_elim
                  (instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
         val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
                    (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
@@ -804,11 +804,11 @@
         val cthp = Simplifier.rewrite (simpset_of ctxt)
             (Thm.capply @{cterm "Trueprop"}
              (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
-        val cth = equal_elim (symmetric cthp) TrueI
-        val rth = implies_elim
+        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
+        val rth = Thm.implies_elim
                  (instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
       in rth end
-    | _ => reflexive ct);
+    | _ => Thm.reflexive ct);
 
 local
   val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"}
@@ -823,7 +823,7 @@
        val nth = Conv.fconv_rule
          (Conv.arg_conv (Conv.arg1_conv
               (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
-       val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
+       val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
 | Const(@{const_name Orderings.less_eq},_)$a$b =>
    let val (ca,cb) = Thm.dest_binop ct
@@ -832,7 +832,7 @@
        val nth = Conv.fconv_rule
          (Conv.arg_conv (Conv.arg1_conv
               (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
-       val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
+       val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
 
 | Const("op =",_)$a$b =>
@@ -842,10 +842,10 @@
        val nth = Conv.fconv_rule
          (Conv.arg_conv (Conv.arg1_conv
               (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
-       val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
+       val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
 | @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
-| _ => reflexive ct
+| _ => Thm.reflexive ct
 end;
 
 fun classfield_whatis phi =
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat May 15 21:50:05 2010 +0200
@@ -106,7 +106,7 @@
       [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
        TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
        TRY (simp_tac simpset3 1), TRY (simp_tac cooper_ss 1)]
-      (trivial ct))
+      (Thm.trivial ct))
     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     (* The result of the quantifier elimination *)
     val (th, tac) = case (prop_of pre_thm) of
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sat May 15 21:50:05 2010 +0200
@@ -87,7 +87,7 @@
    val pre_thm = Seq.hd (EVERY
       [simp_tac simpset0 1,
        TRY (simp_tac (Simplifier.context ctxt ferrack_ss) 1)]
-      (trivial ct))
+      (Thm.trivial ct))
     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     (* The result of the quantifier elimination *)
     val (th, tac) = case prop_of pre_thm of
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat May 15 21:50:05 2010 +0200
@@ -128,7 +128,7 @@
     val pre_thm = Seq.hd (EVERY
       [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
        TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), TRY (simp_tac mir_ss 1)]
-      (trivial ct))
+      (Thm.trivial ct))
     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     (* The result of the quantifier elimination *)
     val (th, tac) = case (prop_of pre_thm) of
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/HOL.thy	Sat May 15 21:50:05 2010 +0200
@@ -1282,12 +1282,12 @@
              else let
                    val abs_g'= Abs (n,xT,g');
                    val g'x = abs_g'$x;
-                   val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x));
+                   val g_g'x = Thm.symmetric (Thm.beta_conversion false (cterm_of thy g'x));
                    val rl = cterm_instantiate
                              [(f_Let_folded, cterm_of thy f), (x_Let_folded, cx),
                               (g_Let_folded, cterm_of thy abs_g')]
                              @{thm Let_folded};
-                 in SOME (rl OF [transitive fx_g g_g'x])
+                 in SOME (rl OF [Thm.transitive fx_g g_g'x])
                  end)
         end
     | _ => NONE)
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Import/import.ML
--- a/src/HOL/Import/import.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Import/import.ML	Sat May 15 21:50:05 2010 +0200
@@ -40,7 +40,7 @@
             val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
             val thm = snd (ProofKernel.to_isa_thm hol4thm)
             val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
-            val thm = equal_elim rew thm
+            val thm = Thm.equal_elim rew thm
             val prew = ProofKernel.rewrite_hol4_term prem thy
             val prem' = #2 (Logic.dest_equals (prop_of prew))
             val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm)
@@ -53,7 +53,7 @@
                     val _ = if prem' aconv (prop_of thm)
                             then message "import: Terms match up"
                             else message "import: Terms DO NOT match up"
-                    val thm' = equal_elim (symmetric prew) thm
+                    val thm' = Thm.equal_elim (Thm.symmetric prew) thm
                     val res = Thm.bicompose true (false,thm',0) 1 th
                 in
                     res
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sat May 15 21:50:05 2010 +0200
@@ -1013,12 +1013,12 @@
 local
     val th = thm "not_def"
     val thy = theory_of_thm th
-    val pp = reflexive (cterm_of thy (Const("Trueprop",boolT-->propT)))
+    val pp = Thm.reflexive (cterm_of thy (Const("Trueprop",boolT-->propT)))
 in
-val not_elim_thm = combination pp th
+val not_elim_thm = Thm.combination pp th
 end
 
-val not_intro_thm = symmetric not_elim_thm
+val not_intro_thm = Thm.symmetric not_elim_thm
 val abs_thm = thm "ext"
 val trans_thm = thm "trans"
 val symmetry_thm = thm "sym"
@@ -1039,7 +1039,7 @@
     end
 
 fun implies_elim_all th =
-    Library.foldl (fn (th,p) => implies_elim th (assume p)) (th,cprems_of th)
+    Library.foldl (fn (th,p) => Thm.implies_elim th (Thm.assume p)) (th,cprems_of th)
 
 fun norm_hyps th =
     th |> beta_eta_thm
@@ -1054,7 +1054,7 @@
         val clc = Thm.cterm_of sg lc
         val cvty = ctyp_of_term cv
         val th1 = implies_elim_all th
-        val th2 = beta_eta_thm (forall_intr cv th1)
+        val th2 = beta_eta_thm (Thm.forall_intr cv th1)
         val th3 = th2 COMP (beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME clc] gen_thm))
         val c = prop_of th3
         val vname = fst(dest_Free v)
@@ -1072,7 +1072,7 @@
 fun rearrange sg tm th =
     let
         val tm' = Envir.beta_eta_contract tm
-        fun find []      n = Thm.permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
+        fun find []      n = Thm.permute_prems 0 1 (Thm.implies_intr (Thm.cterm_of sg tm) th)
           | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p)
                              then Thm.permute_prems n 1 th
                              else find ps (n+1)
@@ -1258,7 +1258,7 @@
 fun get_isabelle_thm thyname thmname hol4conc thy =
     let
         val (info,hol4conc') = disamb_term hol4conc
-        val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
+        val i2h_conc = Thm.symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
         val isaconc =
             case concl_of i2h_conc of
                 Const("==",_) $ lhs $ _ => lhs
@@ -1268,7 +1268,7 @@
                  message "Modified conclusion:";
                  if_debug prin isaconc)
 
-        fun mk_res th = HOLThm(rens_of info,equal_elim i2h_conc th)
+        fun mk_res th = HOLThm (rens_of info, Thm.equal_elim i2h_conc th)
     in
         case get_hol4_mapping thyname thmname thy of
             SOME (SOME thmname) =>
@@ -1320,7 +1320,7 @@
     fun warn () =
         let
             val (info,hol4conc') = disamb_term hol4conc
-            val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
+            val i2h_conc = Thm.symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
         in
             case concl_of i2h_conc of
                 Const("==",_) $ lhs $ _ =>
@@ -1369,7 +1369,7 @@
     let
         val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth
         val rew = rewrite_hol4_term (concl_of th) thy
-        val th  = equal_elim rew th
+        val th  = Thm.equal_elim rew th
         val thy' = add_hol4_pending thyname thmname args thy
         val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
         val th = disambiguate_frees th
@@ -1683,7 +1683,7 @@
         val (info',v') = disamb_term_from info v
         fun strip 0 _ th = th
           | strip n (p::ps) th =
-            strip (n-1) ps (implies_elim th (assume p))
+            strip (n-1) ps (Thm.implies_elim th (Thm.assume p))
           | strip _ _ _ = raise ERR "CHOOSE" "strip error"
         val cv = cterm_of thy v'
         val th2 = norm_hyps th2
@@ -1697,7 +1697,7 @@
         val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
         val th21 = rearrange thy (HOLogic.mk_Trueprop (a $ v')) th2
         val th22 = strip ((nprems_of th21)-1) (cprems_of th21) th21
-        val th23 = beta_eta_thm (forall_intr cv th22)
+        val th23 = beta_eta_thm (Thm.forall_intr cv th22)
         val th11 = implies_elim_all (beta_eta_thm th1)
         val th' = th23 COMP (th11 COMP choose_thm')
         val th = implies_intr_hyps th'
@@ -1796,7 +1796,7 @@
                       | _ => raise ERR "mk_ABS" "Bad conclusion"
         val (fd,fr) = dom_rng (type_of f)
         val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm
-        val th2 = forall_intr cv th1
+        val th2 = Thm.forall_intr cv th1
         val th3 = th2 COMP abs_thm'
         val res = implies_intr_hyps th3
     in
@@ -1867,7 +1867,7 @@
                     _ $ (Const("op -->",_) $ a $ Const("False",_)) => a
                   | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
         val ca = cterm_of thy a
-        val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
+        val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
         val res = HOLThm(rens,implies_intr_hyps th2)
         val _ = message "RESULT:"
         val _ = if_debug pth res
@@ -1884,7 +1884,7 @@
                     _ $ (Const("Not",_) $ a) => a
                   | _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
         val ca = cterm_of thy a
-        val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
+        val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
         val res = HOLThm(rens,implies_intr_hyps th2)
         val _ = message "RESULT:"
         val _ = if_debug pth res
@@ -1902,9 +1902,9 @@
         val prems = prems_of th
         val th1 = beta_eta_thm th
         val th2 = implies_elim_all th1
-        val th3 = implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2
+        val th3 = Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2
         val th4 = th3 COMP disch_thm
-        val res = HOLThm(rens_of info',implies_intr_hyps th4)
+        val res = HOLThm (rens_of info', implies_intr_hyps th4)
         val _ = message "RESULT:"
         val _ = if_debug pth res
     in
@@ -2032,7 +2032,7 @@
             val res' = Thm.unvarify_global res
             val hth = HOLThm(rens,res')
             val rew = rewrite_hol4_term (concl_of res') thy'
-            val th  = equal_elim rew res'
+            val th  = Thm.equal_elim rew res'
             fun handle_const (name,thy) =
                 let
                     val defname = Thm.def_name name
@@ -2112,7 +2112,7 @@
             val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
 
             val rew = rewrite_hol4_term (concl_of td_th) thy4
-            val th  = equal_elim rew (Thm.transfer thy4 td_th)
+            val th  = Thm.equal_elim rew (Thm.transfer thy4 td_th)
             val c   = case HOLogic.dest_Trueprop (prop_of th) of
                           Const("Ex",exT) $ P =>
                           let
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Import/shuffler.ML	Sat May 15 21:50:05 2010 +0200
@@ -95,12 +95,12 @@
         val cQ = cert Q
         val cPQ = cert PQ
         val cPPQ = cert PPQ
-        val th1 = assume cPQ |> implies_intr_list [cPQ,cP]
-        val th3 = assume cP
-        val th4 = implies_elim_list (assume cPPQ) [th3,th3]
+        val th1 = Thm.assume cPQ |> implies_intr_list [cPQ,cP]
+        val th3 = Thm.assume cP
+        val th4 = implies_elim_list (Thm.assume cPPQ) [th3,th3]
                                     |> implies_intr_list [cPPQ,cP]
     in
-        equal_intr th4 th1 |> Drule.export_without_context
+        Thm.equal_intr th4 th1 |> Drule.export_without_context
     end
 
 val imp_comm =
@@ -115,12 +115,12 @@
         val cQ = cert Q
         val cPQR = cert PQR
         val cQPR = cert QPR
-        val th1 = implies_elim_list (assume cPQR) [assume cP,assume cQ]
+        val th1 = implies_elim_list (Thm.assume cPQR) [Thm.assume cP,Thm.assume cQ]
                                     |> implies_intr_list [cPQR,cQ,cP]
-        val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP]
+        val th2 = implies_elim_list (Thm.assume cQPR) [Thm.assume cQ,Thm.assume cP]
                                     |> implies_intr_list [cQPR,cP,cQ]
     in
-        equal_intr th1 th2 |> Drule.export_without_context
+        Thm.equal_intr th1 th2 |> Drule.export_without_context
     end
 
 val def_norm =
@@ -134,20 +134,20 @@
         val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0)))
         val cPQ = cert (Logic.mk_equals(P,Q))
         val cv = cert v
-        val rew = assume cvPQ
-                         |> forall_elim cv
-                         |> abstract_rule "v" cv
+        val rew = Thm.assume cvPQ
+                         |> Thm.forall_elim cv
+                         |> Thm.abstract_rule "v" cv
         val (lhs,rhs) = Logic.dest_equals(concl_of rew)
-        val th1 = transitive (transitive
-                                  (eta_conversion (cert lhs) |> symmetric)
+        val th1 = Thm.transitive (Thm.transitive
+                                  (Thm.eta_conversion (cert lhs) |> Thm.symmetric)
                                   rew)
-                             (eta_conversion (cert rhs))
-                             |> implies_intr cvPQ
-        val th2 = combination (assume cPQ) (reflexive cv)
-                              |> forall_intr cv
-                              |> implies_intr cPQ
+                             (Thm.eta_conversion (cert rhs))
+                             |> Thm.implies_intr cvPQ
+        val th2 = Thm.combination (Thm.assume cPQ) (Thm.reflexive cv)
+                              |> Thm.forall_intr cv
+                              |> Thm.implies_intr cPQ
     in
-        equal_intr th1 th2 |> Drule.export_without_context
+        Thm.equal_intr th1 th2 |> Drule.export_without_context
     end
 
 val all_comm =
@@ -164,16 +164,16 @@
         val cr = cert rhs
         val cx = cert x
         val cy = cert y
-        val th1 = assume cr
+        val th1 = Thm.assume cr
                          |> forall_elim_list [cy,cx]
                          |> forall_intr_list [cx,cy]
-                         |> implies_intr cr
-        val th2 = assume cl
+                         |> Thm.implies_intr cr
+        val th2 = Thm.assume cl
                          |> forall_elim_list [cx,cy]
                          |> forall_intr_list [cy,cx]
-                         |> implies_intr cl
+                         |> Thm.implies_intr cl
     in
-        equal_intr th1 th2 |> Drule.export_without_context
+        Thm.equal_intr th1 th2 |> Drule.export_without_context
     end
 
 val equiv_comm =
@@ -184,10 +184,10 @@
         val u    = Free("u",T)
         val ctu  = cert (Logic.mk_equals(t,u))
         val cut  = cert (Logic.mk_equals(u,t))
-        val th1  = assume ctu |> symmetric |> implies_intr ctu
-        val th2  = assume cut |> symmetric |> implies_intr cut
+        val th1  = Thm.assume ctu |> Thm.symmetric |> Thm.implies_intr ctu
+        val th2  = Thm.assume cut |> Thm.symmetric |> Thm.implies_intr cut
     in
-        equal_intr th1 th2 |> Drule.export_without_context
+        Thm.equal_intr th1 th2 |> Drule.export_without_context
     end
 
 (* This simplification procedure rewrites !!x y. P x y
@@ -217,7 +217,7 @@
         val lhs = list_all ([xv,yv],t)
         val rhs = list_all ([yv,xv],swap_bound 0 t)
         val rew = Logic.mk_equals (lhs,rhs)
-        val init = trivial (cterm_of thy rew)
+        val init = Thm.trivial (cterm_of thy rew)
     in
         (all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
     end
@@ -232,10 +232,10 @@
                  then
                      let
                          val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body)))
-                         val t_th    = reflexive (cterm_of thy t)
-                         val newt_th = reflexive (cterm_of thy newt)
+                         val t_th    = Thm.reflexive (cterm_of thy t)
+                         val newt_th = Thm.reflexive (cterm_of thy newt)
                      in
-                         SOME (transitive t_th newt_th)
+                         SOME (Thm.transitive t_th newt_th)
                      end
                  else NONE
           | _ => error "norm_term (quant_rewrite) internal error"
@@ -294,7 +294,7 @@
 fun eta_contract thy assumes origt =
     let
         val (typet,Tinst) = freeze_thaw_term origt
-        val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet))
+        val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet))
         val final = inst_tfrees thy Tinst o thaw
         val t = #1 (Logic.dest_equals (prop_of init))
         val _ =
@@ -322,18 +322,18 @@
                       val v = Free (Name.variant (Term.add_free_names t []) "v", xT)
                       val cv = cert v
                       val ct = cert t
-                      val th = (assume ct)
-                                   |> forall_elim cv
-                                   |> abstract_rule x cv
-                      val ext_th = eta_conversion (cert (Abs(x,xT,P)))
-                      val th' = transitive (symmetric ext_th) th
+                      val th = (Thm.assume ct)
+                                   |> Thm.forall_elim cv
+                                   |> Thm.abstract_rule x cv
+                      val ext_th = Thm.eta_conversion (cert (Abs(x,xT,P)))
+                      val th' = Thm.transitive (Thm.symmetric ext_th) th
                       val cu = cert (prop_of th')
-                      val uth = combination (assume cu) (reflexive cv)
-                      val uth' = (beta_conversion false (cert (Abs(x,xT,Q) $ v)))
-                                     |> transitive uth
-                                     |> forall_intr cv
-                                     |> implies_intr cu
-                      val rew_th = equal_intr (th' |> implies_intr ct) uth'
+                      val uth = Thm.combination (Thm.assume cu) (Thm.reflexive cv)
+                      val uth' = (Thm.beta_conversion false (cert (Abs(x,xT,Q) $ v)))
+                                     |> Thm.transitive uth
+                                     |> Thm.forall_intr cv
+                                     |> Thm.implies_intr cu
+                      val rew_th = Thm.equal_intr (th' |> Thm.implies_intr ct) uth'
                       val res = final rew_th
                       val lhs = (#1 (Logic.dest_equals (prop_of res)))
                   in
@@ -345,7 +345,7 @@
        end
 
 fun beta_fun thy assume t =
-    SOME (beta_conversion true (cterm_of thy t))
+    SOME (Thm.beta_conversion true (cterm_of thy t))
 
 val meta_sym_rew = thm "refl"
 
@@ -357,7 +357,7 @@
 fun eta_expand thy assumes origt =
     let
         val (typet,Tinst) = freeze_thaw_term origt
-        val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet))
+        val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet))
         val final = inst_tfrees thy Tinst o thaw
         val t = #1 (Logic.dest_equals (prop_of init))
         val _ =
@@ -387,20 +387,20 @@
                           val v = Free(vname,aT)
                           val cv = cert v
                           val ct = cert t
-                          val th1 = (combination (assume ct) (reflexive cv))
-                                        |> forall_intr cv
-                                        |> implies_intr ct
+                          val th1 = (Thm.combination (Thm.assume ct) (Thm.reflexive cv))
+                                        |> Thm.forall_intr cv
+                                        |> Thm.implies_intr ct
                           val concl = cert (concl_of th1)
-                          val th2 = (assume concl)
-                                        |> forall_elim cv
-                                        |> abstract_rule vname cv
+                          val th2 = (Thm.assume concl)
+                                        |> Thm.forall_elim cv
+                                        |> Thm.abstract_rule vname cv
                           val (lhs,rhs) = Logic.dest_equals (prop_of th2)
-                          val elhs = eta_conversion (cert lhs)
-                          val erhs = eta_conversion (cert rhs)
-                          val th2' = transitive
-                                         (transitive (symmetric elhs) th2)
+                          val elhs = Thm.eta_conversion (cert lhs)
+                          val erhs = Thm.eta_conversion (cert rhs)
+                          val th2' = Thm.transitive
+                                         (Thm.transitive (Thm.symmetric elhs) th2)
                                          erhs
-                          val res = equal_intr th1 (th2' |> implies_intr concl)
+                          val res = Thm.equal_intr th1 (th2' |> Thm.implies_intr concl)
                           val res' = final res
                       in
                           SOME res'
@@ -475,7 +475,7 @@
         val (t',_) = F (t,0)
         val ct = cterm_of thy t
         val ct' = cterm_of thy t'
-        val res = transitive (reflexive ct) (reflexive ct')
+        val res = Thm.transitive (Thm.reflexive ct) (Thm.reflexive ct')
         val _ = message ("disamb_term: " ^ (string_of_thm res))
     in
         res
@@ -496,12 +496,12 @@
             let
                 val rhs = Thm.rhs_of th
             in
-                transitive th (f rhs)
+                Thm.transitive th (f rhs)
             end
         val th =
             t |> disamb_bound thy
               |> chain (Simplifier.full_rewrite ss)
-              |> chain eta_conversion
+              |> chain Thm.eta_conversion
               |> Thm.strip_shyps
         val _ = message ("norm_term: " ^ (string_of_thm th))
     in
@@ -529,7 +529,7 @@
     let
         val c = prop_of th
     in
-        equal_elim (norm_term thy c) th
+        Thm.equal_elim (norm_term thy c) th
     end
 
 (* make_equal thy t u tries to construct the theorem t == u under the
@@ -540,7 +540,7 @@
     let
         val t_is_t' = norm_term thy t
         val u_is_u' = norm_term thy u
-        val th = transitive t_is_t' (symmetric u_is_u')
+        val th = Thm.transitive t_is_t' (Thm.symmetric u_is_u')
         val _ = message ("make_equal: SOME " ^ (string_of_thm th))
     in
         SOME th
@@ -593,7 +593,7 @@
           | process ((name,th)::thms) =
             let
                 val norm_th = Thm.varifyT_global (norm_thm thy (close_thm (Thm.transfer thy th)))
-                val triv_th = trivial rhs
+                val triv_th = Thm.trivial rhs
                 val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
                 val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
                                  SOME(th,_) => SOME th
@@ -602,7 +602,7 @@
                 case mod_th of
                     SOME mod_th =>
                     let
-                        val closed_th = equal_elim (symmetric rew_th) mod_th
+                        val closed_th = Thm.equal_elim (Thm.symmetric rew_th) mod_th
                     in
                         message ("Shuffler.set_prop succeeded by " ^ name);
                         SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th)
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Sat May 15 21:50:05 2010 +0200
@@ -1272,7 +1272,7 @@
 fun subst_conv eqs t =
  let
   val t' = fold (Thm.cabs o Thm.lhs_of) eqs t
- in Conv.fconv_rule (Thm.beta_conversion true) (fold (C combination) eqs (reflexive t'))
+ in Conv.fconv_rule (Thm.beta_conversion true) (fold (C Thm.combination) eqs (Thm.reflexive t'))
  end
 
 (* A wrapper that tries to substitute away variables first.                  *)
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Sat May 15 21:50:05 2010 +0200
@@ -182,12 +182,12 @@
 
     (* Some useful derived rules *)
 fun deduct_antisym_rule tha thb = 
-    equal_intr (implies_intr (cprop_of thb) tha) 
-     (implies_intr (cprop_of tha) thb);
+    Thm.equal_intr (Thm.implies_intr (cprop_of thb) tha) 
+     (Thm.implies_intr (cprop_of tha) thb);
 
 fun prove_hyp tha thb = 
   if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb)) 
-  then equal_elim (symmetric (deduct_antisym_rule tha thb)) tha else thb;
+  then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb;
 
 val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and
      "((x = y) == (x - y = 0))" and "((~(x < y)) == (x - y >= 0))" and
@@ -375,7 +375,7 @@
  val skolemize_conv = Simplifier.rewrite (Simplifier.context ctxt skolemize_ss)
  val weak_dnf_ss = HOL_basic_ss addsimps weak_dnf_simps
  val weak_dnf_conv = Simplifier.rewrite (Simplifier.context ctxt weak_dnf_ss)
- fun eqT_elim th = equal_elim (symmetric th) @{thm TrueI}
+ fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI}
  fun oprconv cv ct = 
   let val g = Thm.dest_fun2 ct
   in if g aconvc @{cterm "op <= :: real => _"} 
@@ -387,7 +387,7 @@
   let
    val th' = (Thm.instantiate (Thm.match (Thm.lhs_of th, ct)) th 
       handle MATCH => raise CTERM ("real_ineq_conv", [ct]))
-  in transitive th' (oprconv poly_conv (Thm.rhs_of th'))
+  in Thm.transitive th' (oprconv poly_conv (Thm.rhs_of th'))
   end 
   val [real_lt_conv, real_le_conv, real_eq_conv,
        real_not_lt_conv, real_not_le_conv, _] =
@@ -446,10 +446,10 @@
    let val (p,q) = Thm.dest_binop (concl th)
        val c = concl th1
        val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible"
-   in implies_elim (implies_elim
-          (implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
-          (implies_intr (Thm.capply @{cterm Trueprop} p) th1))
-        (implies_intr (Thm.capply @{cterm Trueprop} q) th2)
+   in Thm.implies_elim (Thm.implies_elim
+          (Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
+          (Thm.implies_intr (Thm.capply @{cterm Trueprop} p) th1))
+        (Thm.implies_intr (Thm.capply @{cterm Trueprop} q) th2)
    end
  fun overall cert_choice dun ths = case ths of
   [] =>
@@ -468,8 +468,8 @@
       overall cert_choice dun (th1::th2::oths) end
     else if is_disj ct then
       let 
-       val (th1, cert1) = overall (Left::cert_choice) dun (assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
-       val (th2, cert2) = overall (Right::cert_choice) dun (assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
+       val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
+       val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
       in (disj_cases th th1 th2, Branch (cert1, cert2)) end
    else overall cert_choice (th::dun) oths
   end
@@ -487,12 +487,12 @@
     val th' = Drule.binop_cong_rule @{cterm "op |"} 
      (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
      (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
-    in transitive th th' 
+    in Thm.transitive th th' 
   end
  fun equal_implies_1_rule PQ = 
   let 
    val P = Thm.lhs_of PQ
-  in implies_intr P (equal_elim PQ (assume P))
+  in Thm.implies_intr P (Thm.equal_elim PQ (Thm.assume P))
   end
  (* FIXME!!! Copied from groebner.ml *)
  val strip_exists =
@@ -507,7 +507,7 @@
  | Var ((s,_),_) => s
  | _ => "x"
 
-  fun mk_forall x th = Drule.arg_cong_rule (instantiate_cterm' [SOME (ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" }) (abstract_rule (name_of x) x th)
+  fun mk_forall x th = Drule.arg_cong_rule (instantiate_cterm' [SOME (ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" }) (Thm.abstract_rule (name_of x) x th)
 
   val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
 
@@ -523,12 +523,12 @@
          (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
      val pv = (Thm.rhs_of o Thm.beta_conversion true) 
            (Thm.capply @{cterm Trueprop} (Thm.capply p v))
-     val th1 = forall_intr v (implies_intr pv th')
-    in implies_elim (implies_elim th0 th) th1  end
+     val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
+    in Thm.implies_elim (Thm.implies_elim th0 th) th1  end
  | _ => raise THM ("choose",0,[th, th'])
 
   fun simple_choose v th = 
-     choose v (assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
+     choose v (Thm.assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
 
  val strip_forall =
   let fun h (acc, t) =
@@ -558,11 +558,11 @@
     val (evs,bod) = strip_exists tm0
     val (avs,ibod) = strip_forall bod
     val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
-    val (th2, certs) = overall [] [] [specl avs (assume (Thm.rhs_of th1))]
-    val th3 = fold simple_choose evs (prove_hyp (equal_elim th1 (assume (Thm.capply @{cterm Trueprop} bod))) th2)
-   in (Drule.implies_intr_hyps (prove_hyp (equal_elim th0 (assume nct)) th3), certs)
+    val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))]
+    val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.capply @{cterm Trueprop} bod))) th2)
+   in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
    end
-  in (implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
+  in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
  end
 in f
 end;
@@ -715,10 +715,10 @@
    fun eliminate_construct p c tm =
     let 
      val t = find_cterm p tm
-     val th0 = (symmetric o beta_conversion false) (Thm.capply (Thm.cabs t tm) t)
+     val th0 = (Thm.symmetric o Thm.beta_conversion false) (Thm.capply (Thm.cabs t tm) t)
      val (p,ax) = (Thm.dest_comb o Thm.rhs_of) th0
-    in fconv_rule(arg_conv(binop_conv (arg_conv (beta_conversion false))))
-               (transitive th0 (c p ax))
+    in fconv_rule(arg_conv(binop_conv (arg_conv (Thm.beta_conversion false))))
+               (Thm.transitive th0 (c p ax))
    end
 
    val elim_abs = eliminate_construct is_abs
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Library/reflection.ML
--- a/src/HOL/Library/reflection.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Library/reflection.ML	Sat May 15 21:50:05 2010 +0200
@@ -133,7 +133,7 @@
                              (AList.update Type.could_unify (HOLogic.listT xT, ((x::bsT), atsT)) bds))
                in (([(ta, ctxt')],
                     fn ([th], bds) =>
-                      (hd (Variable.export ctxt' ctxt [(forall_intr (cert x) th) COMP allI]),
+                      (hd (Variable.export ctxt' ctxt [(Thm.forall_intr (cert x) th) COMP allI]),
                        let val (bsT,asT) = the(AList.lookup Type.could_unify bds (HOLogic.listT xT))
                        in AList.update Type.could_unify (HOLogic.listT xT,(tl bsT,asT)) bds
                        end)),
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Matrix/cplex/matrixlp.ML
--- a/src/HOL/Matrix/cplex/matrixlp.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Matrix/cplex/matrixlp.ML	Sat May 15 21:50:05 2010 +0200
@@ -81,8 +81,8 @@
 fun matrix_simplify th =
     let
         val simp_th = matrix_compute (cprop_of th)
-        val th = Thm.strip_shyps (equal_elim simp_th th)
-        fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th  (* FIXME avoid handle _ *)
+        val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
+        fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle _ => th  (* FIXME avoid handle _ *)
     in
         removeTrue th
     end
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Multivariate_Analysis/normarith.ML
--- a/src/HOL/Multivariate_Analysis/normarith.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Sat May 15 21:50:05 2010 +0200
@@ -80,8 +80,8 @@
 fun replacenegnorms cv t = case term_of t of
   @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
 | @{term "op * :: real => _"}$_$_ =>
-    if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else reflexive t
-| _ => reflexive t
+    if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else Thm.reflexive t
+| _ => Thm.reflexive t
 fun flip v eq =
   if FuncUtil.Ctermfunc.defined eq v
   then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq
@@ -211,7 +211,7 @@
                 ((apply_ptha then_conv vector_add_conv) else_conv
               arg_conv vector_add_conv then_conv apply_pthd)) ct)
       end
-     | _ => reflexive ct))
+     | _ => Thm.reflexive ct))
 
 fun vector_canon_conv ct = case term_of ct of
  Const(@{const_name plus},_)$_$_ =>
@@ -237,7 +237,7 @@
 | Const(@{const_name vec},_)$n =>
   let val n = Thm.dest_arg ct
   in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero)
-     then reflexive ct else apply_pth1 ct
+     then Thm.reflexive ct else apply_pth1 ct
   end
 *)
 | _ => apply_pth1 ct
@@ -342,7 +342,7 @@
   fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
   fun mk_norm t = Thm.capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
   fun mk_equals l r = Thm.capply (Thm.capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
-  val asl = map2 (fn (t,_) => fn n => assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns
+  val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns
   val replace_conv = try_conv (rewrs_conv asl)
   val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv))
   val ges' =
@@ -352,10 +352,10 @@
   val nubs = map (conjunct2 o norm_mp) asl
   val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts')
   val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1))
-  val th11 = hd (Variable.export ctxt' ctxt [fold implies_intr shs th1])
+  val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
   val cps = map (swap o Thm.dest_equals) (cprems_of th11)
   val th12 = instantiate ([], cps) th11
-  val th13 = fold Thm.elim_implies (map (reflexive o snd) cps) th12;
+  val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
  in hd (Variable.export ctxt' ctxt [th13])
  end
 in val real_vector_ineq_prover = real_vector_ineq_prover
@@ -390,7 +390,7 @@
   let
    val ctxt' = Variable.declare_term (term_of ct) ctxt
    val th = init_conv ctxt' ct
-  in equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (symmetric th))
+  in Thm.equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (Thm.symmetric th))
                 (pure ctxt' (Thm.rhs_of th))
  end
 
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sat May 15 21:50:05 2010 +0200
@@ -602,7 +602,7 @@
         (fn _ => EVERY
            [indtac rep_induct [] 1,
             ALLGOALS (simp_tac (global_simpset_of thy4 addsimps
-              (symmetric perm_fun_def :: abs_perm))),
+              (Thm.symmetric perm_fun_def :: abs_perm))),
             ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])),
         length new_type_names));
 
@@ -927,7 +927,7 @@
                simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @
                  constr_defs @ perm_closed_thms)) 1,
                TRY (simp_tac (HOL_basic_ss addsimps
-                 (symmetric perm_fun_def :: abs_perm)) 1),
+                 (Thm.symmetric perm_fun_def :: abs_perm)) 1),
                TRY (simp_tac (HOL_basic_ss addsimps
                  (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
                     perm_closed_thms)) 1)])
@@ -1077,7 +1077,7 @@
          (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
          EVERY (map (fn (prem, r) => (EVERY
            [REPEAT (eresolve_tac Abs_inverse_thms' 1),
-            simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
+            simp_tac (HOL_basic_ss addsimps [Thm.symmetric r]) 1,
             DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
                 (prems ~~ constr_defs))]);
 
@@ -1641,7 +1641,7 @@
                           fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))]
                       supports_fresh) 1,
                     simp_tac (HOL_basic_ss addsimps
-                      [supports_def, symmetric fresh_def, fresh_prod]) 1,
+                      [supports_def, Thm.symmetric fresh_def, fresh_prod]) 1,
                     REPEAT_DETERM (resolve_tac [allI, impI] 1),
                     REPEAT_DETERM (etac conjE 1),
                     rtac unique 1,
@@ -1655,7 +1655,7 @@
                     rtac rec_prem 1,
                     simp_tac (HOL_ss addsimps (fs_name ::
                       supp_prod :: finite_Un :: finite_prems)) 1,
-                    simp_tac (HOL_ss addsimps (symmetric fresh_def ::
+                    simp_tac (HOL_ss addsimps (Thm.symmetric fresh_def ::
                       fresh_prod :: fresh_prems)) 1]
                  end))
           end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ eqvt_ths)
@@ -1746,7 +1746,7 @@
                asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1])
                 (finite_thss ~~ finite_ctxt_ths) @
             maps (fn ((_, idxss), elim) => maps (fn idxs =>
-              [full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff]) 1,
+              [full_simp_tac (HOL_ss addsimps [Thm.symmetric fresh_def, supp_prod, Un_iff]) 1,
                REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1),
                rtac ex1I 1,
                (resolve_tac rec_intrs THEN_ALL_NEW atac) 1,
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Sat May 15 21:50:05 2010 +0200
@@ -266,7 +266,7 @@
 (* intros, then applies eqvt_simp_tac                    *)
 fun supports_tac_i tactical ss i =
   let 
-     val simps        = [supports_def,symmetric fresh_def,fresh_prod]
+     val simps        = [supports_def, Thm.symmetric fresh_def, fresh_prod]
   in
       EVERY [tactical ("unfolding of supports   ", simp_tac (HOL_basic_ss addsimps simps) i),
              tactical ("stripping of foralls    ", REPEAT_DETERM (rtac allI i)),
@@ -329,7 +329,7 @@
         val goal = List.nth(cprems_of st, i-1)
         val fin_supp = dynamic_thms st ("fin_supp")
         val fresh_atm = dynamic_thms st ("fresh_atm")
-        val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
+        val ss1 = ss addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
         val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
     in
       case Logic.strip_assums_concl (term_of goal) of
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML	Sat May 15 21:50:05 2010 +0200
@@ -82,7 +82,7 @@
         val (prems, Const("Trueprop", _)$concl) = rep_goal
                                                 (#3(dest_state (st,i)));
 *)
-        val subgoal = #3(dest_state (st,i));
+        val subgoal = #3(Thm.dest_state (st,i));
         val prems = Logic.strip_assums_hyp subgoal;
         val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
         fun drot_tac k i = DETERM (rotate_tac k i);
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Sat May 15 21:50:05 2010 +0200
@@ -245,7 +245,7 @@
                                       (fn _ => rtac meta_ext 1 THEN 
                                                simp_tac ss1 1);
                      val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1));
-                   in SOME (transitive eq1 eq2) end
+                   in SOME (Thm.transitive eq1 eq2) end
              | _ => NONE)
          end
        | _ => NONE));
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sat May 15 21:50:05 2010 +0200
@@ -483,8 +483,8 @@
            [(indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
             REPEAT (rtac TrueI 1),
             rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
-              symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
-            rewrite_goals_tac (map symmetric range_eqs),
+              Thm.symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
+            rewrite_goals_tac (map Thm.symmetric range_eqs),
             REPEAT (EVERY
               [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
                  maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
@@ -621,7 +621,7 @@
          (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
          EVERY (map (fn (prem, r) => (EVERY
            [REPEAT (eresolve_tac Abs_inverse_thms 1),
-            simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
+            simp_tac (HOL_basic_ss addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
             DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
                 (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
 
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Function/context_tree.ML
--- a/src/HOL/Tools/Function/context_tree.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/Function/context_tree.ML	Sat May 15 21:50:05 2010 +0200
@@ -148,7 +148,7 @@
             val (r, dep, branches) = find_cong_rule ctx fvar h congs_deps t
             fun subtree (ctx', fixes, assumes, st) =
               ((fixes,
-                map (assume o cterm_of (ProofContext.theory_of ctx)) assumes),
+                map (Thm.assume o cterm_of (ProofContext.theory_of ctx)) assumes),
                mk_tree' ctx' st)
           in
             Cong (r, dep, map subtree branches)
@@ -165,7 +165,7 @@
     fun inst_term t =
       subst_bound(f, abstract_over (fvar, t))
 
-    val inst_thm = forall_elim cf o forall_intr cfvar
+    val inst_thm = Thm.forall_elim cf o Thm.forall_intr cfvar
 
     fun inst_tree_aux (Leaf t) = Leaf t
       | inst_tree_aux (Cong (crule, deps, branches)) =
@@ -173,7 +173,7 @@
       | inst_tree_aux (RCall (t, str)) =
         RCall (inst_term t, inst_tree_aux str)
     and inst_branch ((fxs, assms), str) =
-      ((fxs, map (assume o cterm_of thy o inst_term o prop_of) assms),
+      ((fxs, map (Thm.assume o cterm_of thy o inst_term o prop_of) assms),
        inst_tree_aux str)
   in
     inst_tree_aux tr
@@ -188,11 +188,11 @@
  #> fold_rev (Logic.all o Free) fixes
 
 fun export_thm thy (fixes, assumes) =
- fold_rev (implies_intr o cprop_of) assumes
- #> fold_rev (forall_intr o cterm_of thy o Free) fixes
+ fold_rev (Thm.implies_intr o cprop_of) assumes
+ #> fold_rev (Thm.forall_intr o cterm_of thy o Free) fixes
 
 fun import_thm thy (fixes, athms) =
- fold (forall_elim o cterm_of thy o Free) fixes
+ fold (Thm.forall_elim o cterm_of thy o Free) fixes
  #> fold Thm.elim_implies athms
 
 
@@ -241,7 +241,7 @@
 
 fun rewrite_by_tree thy h ih x tr =
   let
-    fun rewrite_help _ _ x (Leaf t) = (reflexive (cterm_of thy t), x)
+    fun rewrite_help _ _ x (Leaf t) = (Thm.reflexive (cterm_of thy t), x)
       | rewrite_help fix h_as x (RCall (_ $ arg, st)) =
         let
           val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *)
@@ -250,11 +250,11 @@
             |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
                                                     (* (a, h a) : G   *)
           val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
-          val eq = implies_elim (implies_elim inst_ih lRi) iha (* h a = f a *)
+          val eq = Thm.implies_elim (Thm.implies_elim inst_ih lRi) iha (* h a = f a *)
 
-          val h_a'_eq_h_a = combination (reflexive (cterm_of thy h)) inner
+          val h_a'_eq_h_a = Thm.combination (Thm.reflexive (cterm_of thy h)) inner
           val h_a_eq_f_a = eq RS eq_reflection
-          val result = transitive h_a'_eq_h_a h_a_eq_f_a
+          val result = Thm.transitive h_a'_eq_h_a h_a_eq_f_a
         in
           (result, x')
         end
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sat May 15 21:50:05 2010 +0200
@@ -154,9 +154,9 @@
     val rhs = inst pre_rhs
 
     val cqs = map (cterm_of thy) qs
-    val ags = map (assume o cterm_of thy) gs
+    val ags = map (Thm.assume o cterm_of thy) gs
 
-    val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
+    val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
   in
     ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
       cqs = cqs, ags = ags, case_hyp = case_hyp }
@@ -188,15 +188,15 @@
 
     (* Instantiate the GIntro thm with "f" and import into the clause context. *)
     val lGI = GIntro_thm
-      |> forall_elim (cert f)
-      |> fold forall_elim cqs
+      |> Thm.forall_elim (cert f)
+      |> fold Thm.forall_elim cqs
       |> fold Thm.elim_implies ags
 
     fun mk_call_info (rcfix, rcassm, rcarg) RI =
       let
         val llRI = RI
-          |> fold forall_elim cqs
-          |> fold (forall_elim o cert o Free) rcfix
+          |> fold Thm.forall_elim cqs
+          |> fold (Thm.forall_elim o cert o Free) rcfix
           |> fold Thm.elim_implies ags
           |> fold Thm.elim_implies rcassm
 
@@ -242,20 +242,20 @@
       val compat = lookup_compat_thm j i cts
     in
       compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
-      |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
+      |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
       |> fold Thm.elim_implies agsj
       |> fold Thm.elim_implies agsi
-      |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
+      |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
     end
     else
     let
       val compat = lookup_compat_thm i j cts
     in
       compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
-      |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
+      |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
       |> fold Thm.elim_implies agsi
       |> fold Thm.elim_implies agsj
-      |> Thm.elim_implies (assume lhsi_eq_lhsj)
+      |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
       |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
     end
   end
@@ -274,16 +274,16 @@
 
     val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
     val h_assums = map (fn RCInfo {h_assum, ...} =>
-      assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
+      Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
 
     val (eql, _) =
       Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
 
     val replace_lemma = (eql RS meta_eq_to_obj_eq)
-      |> implies_intr (cprop_of case_hyp)
-      |> fold_rev (implies_intr o cprop_of) h_assums
-      |> fold_rev (implies_intr o cprop_of) ags
-      |> fold_rev forall_intr cqs
+      |> Thm.implies_intr (cprop_of case_hyp)
+      |> fold_rev (Thm.implies_intr o cprop_of) h_assums
+      |> fold_rev (Thm.implies_intr o cprop_of) ags
+      |> fold_rev Thm.forall_intr cqs
       |> Thm.close_derivation
   in
     replace_lemma
@@ -301,30 +301,30 @@
 
     val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
     val compat = get_compat_thm thy compat_store i j cctxi cctxj
-    val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
+    val Ghsj' = map (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
 
     val RLj_import = RLj
-      |> fold forall_elim cqsj'
+      |> fold Thm.forall_elim cqsj'
       |> fold Thm.elim_implies agsj'
       |> fold Thm.elim_implies Ghsj'
 
-    val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
-    val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
+    val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
+    val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
        (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
   in
     (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
-    |> implies_elim RLj_import
+    |> Thm.implies_elim RLj_import
       (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
     |> (fn it => trans OF [it, compat])
       (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
     |> (fn it => trans OF [y_eq_rhsj'h, it])
       (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
-    |> fold_rev (implies_intr o cprop_of) Ghsj'
-    |> fold_rev (implies_intr o cprop_of) agsj'
+    |> fold_rev (Thm.implies_intr o cprop_of) Ghsj'
+    |> fold_rev (Thm.implies_intr o cprop_of) agsj'
       (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
-    |> implies_intr (cprop_of y_eq_rhsj'h)
-    |> implies_intr (cprop_of lhsi_eq_lhsj')
-    |> fold_rev forall_intr (cterm_of thy h :: cqsj')
+    |> Thm.implies_intr (cprop_of y_eq_rhsj'h)
+    |> Thm.implies_intr (cprop_of lhsi_eq_lhsj')
+    |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')
   end
 
 
@@ -338,13 +338,13 @@
     val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
 
     fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
-      |> fold_rev (implies_intr o cprop_of) CCas
-      |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+      |> fold_rev (Thm.implies_intr o cprop_of) CCas
+      |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
 
     val existence = fold (curry op COMP o prep_RC) RCs lGI
 
     val P = cterm_of thy (mk_eq (y, rhsC))
-    val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
+    val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
 
     val unique_clauses =
       map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
@@ -353,13 +353,13 @@
       Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
 
     val uniqueness = G_cases
-      |> forall_elim (cterm_of thy lhs)
-      |> forall_elim (cterm_of thy y)
-      |> forall_elim P
+      |> Thm.forall_elim (cterm_of thy lhs)
+      |> Thm.forall_elim (cterm_of thy y)
+      |> Thm.forall_elim P
       |> Thm.elim_implies G_lhs_y
       |> fold elim_implies_eta unique_clauses
-      |> implies_intr (cprop_of G_lhs_y)
-      |> forall_intr (cterm_of thy y)
+      |> Thm.implies_intr (cprop_of G_lhs_y)
+      |> Thm.forall_intr (cterm_of thy y)
 
     val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
 
@@ -368,16 +368,16 @@
       |> curry (op COMP) existence
       |> curry (op COMP) uniqueness
       |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
-      |> implies_intr (cprop_of case_hyp)
-      |> fold_rev (implies_intr o cprop_of) ags
-      |> fold_rev forall_intr cqs
+      |> Thm.implies_intr (cprop_of case_hyp)
+      |> fold_rev (Thm.implies_intr o cprop_of) ags
+      |> fold_rev Thm.forall_intr cqs
 
     val function_value =
       existence
-      |> implies_intr ihyp
-      |> implies_intr (cprop_of case_hyp)
-      |> forall_intr (cterm_of thy x)
-      |> forall_elim (cterm_of thy lhs)
+      |> Thm.implies_intr ihyp
+      |> Thm.implies_intr (cprop_of case_hyp)
+      |> Thm.forall_intr (cterm_of thy x)
+      |> Thm.forall_elim (cterm_of thy lhs)
       |> curry (op RS) refl
   in
     (exactly_one, function_value)
@@ -396,7 +396,7 @@
           Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
       |> cterm_of thy
 
-    val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0
+    val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
     val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
     val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
       |> instantiate' [] [NONE, SOME (cterm_of thy h)]
@@ -412,17 +412,17 @@
     val graph_is_function = complete
       |> Thm.forall_elim_vars 0
       |> fold (curry op COMP) ex1s
-      |> implies_intr (ihyp)
-      |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
-      |> forall_intr (cterm_of thy x)
+      |> Thm.implies_intr (ihyp)
+      |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
+      |> Thm.forall_intr (cterm_of thy x)
       |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
-      |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
+      |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
 
     val goalstate =  Conjunction.intr graph_is_function complete
       |> Thm.close_derivation
       |> Goal.protect
-      |> fold_rev (implies_intr o cprop_of) compat
-      |> implies_intr (cprop_of complete)
+      |> fold_rev (Thm.implies_intr o cprop_of) compat
+      |> Thm.implies_intr (cprop_of complete)
   in
     (goalstate, values)
   end
@@ -544,7 +544,7 @@
   let
     fun inst_term t = subst_bound(f, abstract_over (fvar, t))
   in
-    (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
+    (rcfix, map (Thm.assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
   end
 
 
@@ -562,14 +562,14 @@
         val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
         val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
       in
-        ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
+        ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward))
         |> (fn it => it COMP graph_is_function)
-        |> implies_intr z_smaller
-        |> forall_intr (cterm_of thy z)
+        |> Thm.implies_intr z_smaller
+        |> Thm.forall_intr (cterm_of thy z)
         |> (fn it => it COMP valthm)
-        |> implies_intr lhs_acc
+        |> Thm.implies_intr lhs_acc
         |> asm_simplify (HOL_basic_ss addsimps [f_iff])
-        |> fold_rev (implies_intr o cprop_of) ags
+        |> fold_rev (Thm.implies_intr o cprop_of) ags
         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
       end
   in
@@ -588,7 +588,7 @@
     val Globals {domT, x, z, a, P, D, ...} = globals
     val acc_R = mk_acc domT R
 
-    val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
+    val x_D = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
     val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
 
     val D_subset = cterm_of thy (Logic.all x
@@ -606,7 +606,7 @@
         HOLogic.mk_Trueprop (P $ Bound 0)))
       |> cterm_of thy
 
-    val aihyp = assume ihyp
+    val aihyp = Thm.assume ihyp
 
     fun prove_case clause =
       let
@@ -622,10 +622,10 @@
         end
 
         fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
-          |> forall_elim (cterm_of thy rcarg)
+          |> Thm.forall_elim (cterm_of thy rcarg)
           |> Thm.elim_implies llRI
-          |> fold_rev (implies_intr o cprop_of) CCas
-          |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+          |> fold_rev (Thm.implies_intr o cprop_of) CCas
+          |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
 
         val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
 
@@ -636,19 +636,19 @@
           |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
           |> cterm_of thy
 
-        val P_lhs = assume step
-          |> fold forall_elim cqs
+        val P_lhs = Thm.assume step
+          |> fold Thm.forall_elim cqs
           |> Thm.elim_implies lhs_D
           |> fold Thm.elim_implies ags
           |> fold Thm.elim_implies P_recs
 
         val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
           |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
-          |> symmetric (* P lhs == P x *)
-          |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
-          |> implies_intr (cprop_of case_hyp)
-          |> fold_rev (implies_intr o cprop_of) ags
-          |> fold_rev forall_intr cqs
+          |> Thm.symmetric (* P lhs == P x *)
+          |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *)
+          |> Thm.implies_intr (cprop_of case_hyp)
+          |> fold_rev (Thm.implies_intr o cprop_of) ags
+          |> fold_rev Thm.forall_intr cqs
       in
         (res, step)
       end
@@ -658,33 +658,33 @@
     val istep = complete_thm
       |> Thm.forall_elim_vars 0
       |> fold (curry op COMP) cases (*  P x  *)
-      |> implies_intr ihyp
-      |> implies_intr (cprop_of x_D)
-      |> forall_intr (cterm_of thy x)
+      |> Thm.implies_intr ihyp
+      |> Thm.implies_intr (cprop_of x_D)
+      |> Thm.forall_intr (cterm_of thy x)
 
     val subset_induct_rule =
       acc_subset_induct
-      |> (curry op COMP) (assume D_subset)
-      |> (curry op COMP) (assume D_dcl)
-      |> (curry op COMP) (assume a_D)
+      |> (curry op COMP) (Thm.assume D_subset)
+      |> (curry op COMP) (Thm.assume D_dcl)
+      |> (curry op COMP) (Thm.assume a_D)
       |> (curry op COMP) istep
-      |> fold_rev implies_intr steps
-      |> implies_intr a_D
-      |> implies_intr D_dcl
-      |> implies_intr D_subset
+      |> fold_rev Thm.implies_intr steps
+      |> Thm.implies_intr a_D
+      |> Thm.implies_intr D_dcl
+      |> Thm.implies_intr D_subset
 
     val simple_induct_rule =
       subset_induct_rule
-      |> forall_intr (cterm_of thy D)
-      |> forall_elim (cterm_of thy acc_R)
+      |> Thm.forall_intr (cterm_of thy D)
+      |> Thm.forall_elim (cterm_of thy acc_R)
       |> assume_tac 1 |> Seq.hd
       |> (curry op COMP) (acc_downward
         |> (instantiate' [SOME (ctyp_of thy domT)]
              (map (SOME o cterm_of thy) [R, x, z]))
-        |> forall_intr (cterm_of thy z)
-        |> forall_intr (cterm_of thy x))
-      |> forall_intr (cterm_of thy a)
-      |> forall_intr (cterm_of thy P)
+        |> Thm.forall_intr (cterm_of thy z)
+        |> Thm.forall_intr (cterm_of thy x))
+      |> Thm.forall_intr (cterm_of thy a)
+      |> Thm.forall_intr (cterm_of thy P)
   in
     simple_induct_rule
   end
@@ -736,18 +736,19 @@
           |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
           |> cterm_of thy
 
-        val thm = assume hyp
-          |> fold forall_elim cqs
+        val thm = Thm.assume hyp
+          |> fold Thm.forall_elim cqs
           |> fold Thm.elim_implies ags
           |> Function_Ctx_Tree.import_thm thy (fixes, assumes)
           |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
 
         val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg))
-          |> cterm_of thy |> assume
+          |> cterm_of thy |> Thm.assume
 
         val acc = thm COMP ih_case
         val z_acc_local = acc
-          |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
+          |> Conv.fconv_rule
+              (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection)))))
 
         val ethm = z_acc_local
           |> Function_Ctx_Tree.export_thm thy (fixes,
@@ -785,34 +786,34 @@
         HOLogic.mk_Trueprop (acc_R $ Bound 0)))
       |> cterm_of thy
 
-    val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
+    val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0
 
     val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
 
     val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], [])
   in
     R_cases
-    |> forall_elim (cterm_of thy z)
-    |> forall_elim (cterm_of thy x)
-    |> forall_elim (cterm_of thy (acc_R $ z))
-    |> curry op COMP (assume R_z_x)
+    |> Thm.forall_elim (cterm_of thy z)
+    |> Thm.forall_elim (cterm_of thy x)
+    |> Thm.forall_elim (cterm_of thy (acc_R $ z))
+    |> curry op COMP (Thm.assume R_z_x)
     |> fold_rev (curry op COMP) cases
-    |> implies_intr R_z_x
-    |> forall_intr (cterm_of thy z)
+    |> Thm.implies_intr R_z_x
+    |> Thm.forall_intr (cterm_of thy z)
     |> (fn it => it COMP accI)
-    |> implies_intr ihyp
-    |> forall_intr (cterm_of thy x)
+    |> Thm.implies_intr ihyp
+    |> Thm.forall_intr (cterm_of thy x)
     |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
-    |> curry op RS (assume wfR')
+    |> curry op RS (Thm.assume wfR')
     |> forall_intr_vars
     |> (fn it => it COMP allI)
-    |> fold implies_intr hyps
-    |> implies_intr wfR'
-    |> forall_intr (cterm_of thy R')
-    |> forall_elim (cterm_of thy (inrel_R))
+    |> fold Thm.implies_intr hyps
+    |> Thm.implies_intr wfR'
+    |> Thm.forall_intr (cterm_of thy R')
+    |> Thm.forall_elim (cterm_of thy (inrel_R))
     |> curry op RS wf_in_rel
     |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
-    |> forall_intr (cterm_of thy Rrel)
+    |> Thm.forall_intr (cterm_of thy Rrel)
   end
 
 
@@ -919,11 +920,11 @@
         RCss GIntro_thms) RIntro_thmss
 
     val complete =
-      mk_completeness globals clauses abstract_qglrs |> cert |> assume
+      mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume
 
     val compat =
       mk_compat_proof_obligations domT ranT fvar f abstract_qglrs
-      |> map (cert #> assume)
+      |> map (cert #> Thm.assume)
 
     val compat_store = store_compat_thms n compat
 
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Sat May 15 21:50:05 2010 +0200
@@ -5,7 +5,7 @@
 Some fairly general functions that should probably go somewhere else...
 *)
 
-structure Function_Lib =
+structure Function_Lib =   (* FIXME proper signature *)
 struct
 
 fun map_option f NONE = NONE
@@ -104,7 +104,7 @@
 
 fun forall_intr_rename (n, cv) thm =
   let
-    val allthm = forall_intr cv thm
+    val allthm = Thm.forall_intr cv thm
     val (_ $ abs) = prop_of allthm
   in
     Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Sat May 15 21:50:05 2010 +0200
@@ -226,7 +226,7 @@
          HOLogic.mk_Trueprop (P_comp $ Bound 0)))
       |> cert
 
-    val aihyp = assume ihyp
+    val aihyp = Thm.assume ihyp
 
     (* Rule for case splitting along the sum types *)
     val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
@@ -237,9 +237,9 @@
     fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
       let
         val fxs = map Free xs
-        val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
+        val branch_hyp = Thm.assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
 
-        val C_hyps = map (cert #> assume) Cs
+        val C_hyps = map (cert #> Thm.assume) Cs
 
         val (relevant_cases, ineqss') =
           (scases_idx ~~ ineqss)
@@ -248,32 +248,33 @@
 
         fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
           let
-            val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
+            val case_hyps =
+              map (Thm.assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
 
             val cqs = map (cert o Free) qs
-            val ags = map (assume o cert) gs
+            val ags = map (Thm.assume o cert) gs
 
             val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
             val sih = full_simplify replace_x_ss aihyp
 
             fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
               let
-                val cGas = map (assume o cert) Gas
+                val cGas = map (Thm.assume o cert) Gas
                 val cGvs = map (cert o Free) Gvs
-                val import = fold forall_elim (cqs @ cGvs)
+                val import = fold Thm.forall_elim (cqs @ cGvs)
                   #> fold Thm.elim_implies (ags @ cGas)
                 val ipres = pres
-                  |> forall_elim (cert (list_comb (P_of idx, rcargs)))
+                  |> Thm.forall_elim (cert (list_comb (P_of idx, rcargs)))
                   |> import
               in
                 sih
-                |> forall_elim (cert (inject idx rcargs))
+                |> Thm.forall_elim (cert (inject idx rcargs))
                 |> Thm.elim_implies (import ineq) (* Psum rcargs *)
                 |> Conv.fconv_rule sum_prod_conv
                 |> Conv.fconv_rule ind_rulify
                 |> (fn th => th COMP ipres) (* P rs *)
-                |> fold_rev (implies_intr o cprop_of) cGas
-                |> fold_rev forall_intr cGvs
+                |> fold_rev (Thm.implies_intr o cprop_of) cGas
+                |> fold_rev Thm.forall_intr cGvs
               end
 
             val P_recs = map2 mk_Prec rs ineq_press   (*  [P rec1, P rec2, ... ]  *)
@@ -288,13 +289,13 @@
               foldl1 (uncurry Conv.combination_conv)
                 (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps)
 
-            val res = assume step
-              |> fold forall_elim cqs
+            val res = Thm.assume step
+              |> fold Thm.forall_elim cqs
               |> fold Thm.elim_implies ags
               |> fold Thm.elim_implies P_recs (* P lhs *)
               |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *)
-              |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps)
-              |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
+              |> fold_rev (Thm.implies_intr o cprop_of) (ags @ case_hyps)
+              |> fold_rev Thm.forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
           in
             (res, (cidx, step))
           end
@@ -302,12 +303,12 @@
         val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
 
         val bstep = complete_thm
-          |> forall_elim (cert (list_comb (P, fxs)))
-          |> fold (forall_elim o cert) (fxs @ map Free ws)
+          |> Thm.forall_elim (cert (list_comb (P, fxs)))
+          |> fold (Thm.forall_elim o cert) (fxs @ map Free ws)
           |> fold Thm.elim_implies C_hyps
           |> fold Thm.elim_implies cases (* P xs *)
-          |> fold_rev (implies_intr o cprop_of) C_hyps
-          |> fold_rev (forall_intr o cert o Free) ws
+          |> fold_rev (Thm.implies_intr o cprop_of) C_hyps
+          |> fold_rev (Thm.forall_intr o cert o Free) ws
 
         val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
           |> Goal.init
@@ -316,8 +317,8 @@
           |> Seq.hd
           |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
           |> Goal.finish ctxt
-          |> implies_intr (cprop_of branch_hyp)
-          |> fold_rev (forall_intr o cert) fxs
+          |> Thm.implies_intr (cprop_of branch_hyp)
+          |> fold_rev (Thm.forall_intr o cert) fxs
       in
         (Pxs, steps)
       end
@@ -328,8 +329,8 @@
 
     val istep = sum_split_rule
       |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
-      |> implies_intr ihyp
-      |> forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
+      |> Thm.implies_intr ihyp
+      |> Thm.forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
 
     val induct_rule =
       @{thm "wf_induct_rule"}
@@ -353,10 +354,10 @@
     val cert = cterm_of (ProofContext.theory_of ctxt)
 
     val ineqss = mk_ineqs R scheme
-      |> map (map (pairself (assume o cert)))
+      |> map (map (pairself (Thm.assume o cert)))
     val complete =
-      map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
-    val wf_thm = mk_wf R scheme |> cert |> assume
+      map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches)
+    val wf_thm = mk_wf R scheme |> cert |> Thm.assume
 
     val (descent, pres) = split_list (flat ineqss)
     val newgoals = complete @ pres @ wf_thm :: descent
@@ -377,7 +378,7 @@
       end
 
     val res = Conjunction.intr_balanced (map_index project branches)
-      |> fold_rev implies_intr (map cprop_of newgoals @ steps)
+      |> fold_rev Thm.implies_intr (map cprop_of newgoals @ steps)
       |> Drule.generalize ([], [Rn])
 
     val nbranches = length branches
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Sat May 15 21:50:05 2010 +0200
@@ -164,12 +164,12 @@
     val rhs = inst pre_rhs
 
     val cqs = map (cterm_of thy) qs
-    val ags = map (assume o cterm_of thy) gs
+    val ags = map (Thm.assume o cterm_of thy) gs
 
-    val import = fold forall_elim cqs
+    val import = fold Thm.forall_elim cqs
       #> fold Thm.elim_implies ags
 
-    val export = fold_rev (implies_intr o cprop_of) ags
+    val export = fold_rev (Thm.implies_intr o cprop_of) ags
       #> fold_rev forall_intr_rename (oqnames ~~ cqs)
   in
     F ctxt (f, qs, gs, args, rhs) import export
@@ -184,7 +184,7 @@
     val (simp, restore_cond) =
       case cprems_of psimp of
         [] => (psimp, I)
-      | [cond] => (implies_elim psimp (assume cond), implies_intr cond)
+      | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
       | _ => sys_error "Too many conditions"
 
   in
@@ -202,9 +202,9 @@
     val thy = ProofContext.theory_of ctxt
     val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
   in
-    fold (fn x => fn thm => combination thm (reflexive x)) xs thm
+    fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm
     |> Conv.fconv_rule (Thm.beta_conversion true)
-    |> fold_rev forall_intr xs
+    |> fold_rev Thm.forall_intr xs
     |> Thm.forall_elim_vars 0
   end
 
@@ -228,7 +228,7 @@
     val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps
 
     val induct_inst =
-      forall_elim (cert case_exp) induct
+      Thm.forall_elim (cert case_exp) induct
       |> full_simplify SumTree.sumcase_split_ss
       |> full_simplify (HOL_basic_ss addsimps all_f_defs)
 
@@ -238,9 +238,9 @@
         val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
       in
         (rule
-         |> forall_elim (cert inj)
+         |> Thm.forall_elim (cert inj)
          |> full_simplify SumTree.sumcase_split_ss
-         |> fold_rev (forall_intr o cert) (afs @ newPs),
+         |> fold_rev (Thm.forall_intr o cert) (afs @ newPs),
          k + length cargTs)
       end
   in
@@ -255,7 +255,7 @@
 
     val (all_f_defs, fs) =
       map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
-        (mk_applied_form lthy cargTs (symmetric f_def), f))
+        (mk_applied_form lthy cargTs (Thm.symmetric f_def), f))
       parts
       |> split_list
 
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Function/pat_completeness.ML
--- a/src/HOL/Tools/Function/pat_completeness.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/Function/pat_completeness.ML	Sat May 15 21:50:05 2010 +0200
@@ -24,7 +24,7 @@
 fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
 fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
 
-fun inst_free var inst = forall_elim inst o forall_intr var
+fun inst_free var inst = Thm.forall_elim inst o Thm.forall_intr var
 
 fun inst_case_thm thy x P thm =
   let val [Pv, xv] = Term.add_vars (prop_of thm) []
@@ -69,10 +69,10 @@
   let
     val (_, subps) = strip_comb pat
     val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
-    val c_eq_pat = simplify (HOL_basic_ss addsimps (map assume eqs)) c_assum
+    val c_eq_pat = simplify (HOL_basic_ss addsimps (map Thm.assume eqs)) c_assum
   in
     (subps @ pats,
-     fold_rev implies_intr eqs (implies_elim thm c_eq_pat))
+     fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat))
   end
 
 
@@ -82,12 +82,12 @@
   let
     val (avars, pvars, newidx) = invent_vars cons idx
     val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
-    val c_assum = assume c_hyp
+    val c_assum = Thm.assume c_hyp
     val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats)
   in
     o_alg thy P newidx (avars @ vs) newpats
-    |> implies_intr c_hyp
-    |> fold_rev (forall_intr o cterm_of thy) avars
+    |> Thm.implies_intr c_hyp
+    |> fold_rev (Thm.forall_intr o cterm_of thy) avars
   end
   | constr_case _ _ _ _ _ _ = raise Match
 and o_alg thy P idx [] (([], Pthm) :: _)  = Pthm
@@ -119,11 +119,11 @@
       |> cterm_of thy
 
     val hyps = map2 mk_assum qss patss
-    fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp)
+    fun inst_hyps hyp qs = fold (Thm.forall_elim o cterm_of thy) qs (Thm.assume hyp)
     val assums = map2 inst_hyps hyps qss
     in
       o_alg thy P 2 xs (patss ~~ assums)
-      |> fold_rev implies_intr hyps
+      |> fold_rev Thm.implies_intr hyps
     end
 
 fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) =>
@@ -147,7 +147,7 @@
 
     val patss = map (map snd) x_pats
     val complete_thm = prove_completeness thy xs thesis qss patss
-      |> fold_rev (forall_intr o cterm_of thy) vs
+      |> fold_rev (Thm.forall_intr o cterm_of thy) vs
     in
       PRIMITIVE (fn st => Drule.compose_single(complete_thm, i, st))
   end
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sat May 15 21:50:05 2010 +0200
@@ -331,7 +331,7 @@
 | t => if is_intrel t
       then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop))
        RS eq_reflection
-      else reflexive ct;
+      else Thm.reflexive ct;
 
 val dvdc = @{cterm "op dvd :: int => _"};
 
@@ -369,7 +369,7 @@
       (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}
            (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
            @{cterm "0::int"})))
-   in equal_elim (Thm.symmetric th) TrueI end;
+   in Thm.equal_elim (Thm.symmetric th) TrueI end;
   val notz =
     let val tab = fold Inttab.update
           (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
@@ -412,11 +412,11 @@
   val ltx = Thm.capply (Thm.capply cmulC clt) cx
   val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth)
   val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex
-  val thf = transitive th
-      (transitive (symmetric (beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
+  val thf = Thm.transitive th
+      (Thm.transitive (Thm.symmetric (Thm.beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
   val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true
-                  ||> beta_conversion true |>> Thm.symmetric
- in transitive (transitive lth thf) rth end;
+                  ||> Thm.beta_conversion true |>> Thm.symmetric
+ in Thm.transitive (Thm.transitive lth thf) rth end;
 
 
 val emptyIS = @{cterm "{}::int set"};
@@ -459,7 +459,7 @@
      Simplifier.rewrite lin_ss
       (Thm.capply @{cterm Trueprop}
            (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
-   in equal_elim (Thm.symmetric th) TrueI end;
+   in Thm.equal_elim (Thm.symmetric th) TrueI end;
  val dvd =
    let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
      fn ct => the (Inttab.lookup tab (term_of ct |> dest_number))
@@ -471,7 +471,7 @@
    let val th = Simplifier.rewrite lin_ss
       (Thm.capply @{cterm Trueprop}
            (Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
-   in equal_elim (Thm.symmetric th) TrueI end;
+   in Thm.equal_elim (Thm.symmetric th) TrueI end;
     (* A and B set *)
    local
      val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
@@ -483,7 +483,7 @@
       | Const(@{const_name insert}, _) $ y $ _ =>
          let val (cy,S') = Thm.dest_binop S
          in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
-         else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
+         else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
                            (provein x S')
          end
    end
@@ -494,14 +494,14 @@
    if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)
    then
     (bl,b0,decomp_minf,
-     fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
+     fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
                      [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@
                    (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]))
                         [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj,
                          bsetdisj,infDconj, infDdisj]),
                        cpmi)
      else (al,a0,decomp_pinf,fn A =>
-          (map (fn th => implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
+          (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
                    [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@
                    (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]))
                    [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,
@@ -776,7 +776,7 @@
    fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
    val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
    val p' = fold_rev gen ts p
- in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
+ in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
 
 local
 val ss1 = comp_ss
@@ -792,7 +792,7 @@
             @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
   addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
 val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms}
-  @ map (symmetric o mk_meta_eq) 
+  @ map (Thm.symmetric o mk_meta_eq) 
     [@{thm "dvd_eq_mod_eq_0"},
      @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
      @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
@@ -823,7 +823,7 @@
        then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
        else Conv.arg_conv (conv ctxt) p
     val p' = Thm.rhs_of cpth
-    val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
+    val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
    in rtac th i end
    handle COOPER _ => no_tac);
 
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Qelim/ferrante_rackoff.ML
--- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Sat May 15 21:50:05 2010 +0200
@@ -69,7 +69,7 @@
       val th0 = if mi then
            instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
         else instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
-     in implies_elim (implies_elim th0 th') th'' end
+     in Thm.implies_elim (Thm.implies_elim th0 th') th'' end
   in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
       fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
   end
@@ -88,7 +88,7 @@
    val enth = Drule.arg_cong_rule ce nthx
    val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
    fun ins x th =
-      implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
+      Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
                                        (Thm.cprop_of th), SOME x] th1) th
    val fU = fold ins u th0
    val cU = funpow 2 Thm.dest_arg (Thm.cprop_of fU)
@@ -102,7 +102,7 @@
       | Const(@{const_name insert}, _) $ y $_ =>
          let val (cy,S') = Thm.dest_binop S
          in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
-         else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
+         else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
                            (provein x S')
          end
    end
@@ -152,7 +152,7 @@
                           | Eq => [minf_eq, pinf_eq, nmi_eq, npi_eq, ld_eq]
                           | NEq => [minf_neq, pinf_neq, nmi_neq, npi_neq, ld_neq])
                     val tU = U t
-                    fun Ufw th = implies_elim th tU
+                    fun Ufw th = Thm.implies_elim th tU
                  in [mi_th, pi_th, Ufw nmi_th, Ufw npi_th, Ufw ld_th]
                  end
          in ([], K (mi_th, pi_th, nmi_th, npi_th, ld_th)) end)
@@ -164,7 +164,7 @@
                   [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
     val bex_conv =
       Simplifier.rewrite (HOL_basic_ss addsimps simp_thms@(@{thms "bex_simps" (1-5)}))
-    val result_th = fconv_rule (arg_conv bex_conv) (transitive enth qe_th)
+    val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th)
    in result_th
    end
 
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Qelim/langford.ML
--- a/src/HOL/Tools/Qelim/langford.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/Qelim/langford.ML	Sat May 15 21:50:05 2010 +0200
@@ -22,7 +22,7 @@
 fun prove_finite cT u = 
 let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
     fun ins x th =
-     implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
+     Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
                                      (Thm.cprop_of th), SOME x] th1) th
 in fold ins u th0 end;
 
@@ -51,17 +51,17 @@
       (Const (@{const_name Orderings.bot}, _),_) =>  
         let
           val (neU,fU) = proveneF U 
-        in simp_rule (transitive ths (dlo_qeth_nolb OF [neU, fU])) end
+        in simp_rule (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
     | (_,Const (@{const_name Orderings.bot}, _)) =>  
         let
           val (neL,fL) = proveneF L
-        in simp_rule (transitive ths (dlo_qeth_noub OF [neL, fL])) end
+        in simp_rule (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
 
     | (_,_) =>  
       let 
        val (neL,fL) = proveneF L
        val (neU,fU) = proveneF U
-      in simp_rule (transitive ths (dlo_qeth OF [neL, neU, fL, fU])) 
+      in simp_rule (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU])) 
       end
    in qe end 
  | _ => error "dlo_qe : Not an existential formula";
@@ -101,8 +101,8 @@
 fun conj_aci_rule eq = 
  let 
   val (l,r) = Thm.dest_equals eq
-  fun tabl c = the (Termtab.lookup (mk_conj_tab (assume l)) (term_of c))
-  fun tabr c = the (Termtab.lookup (mk_conj_tab (assume r)) (term_of c))
+  fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c))
+  fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c))
   val ll = Thm.dest_arg l
   val rr = Thm.dest_arg r
   
@@ -111,7 +111,7 @@
   val thr  = prove_conj tabr (conjuncts ll) 
                 |> Drule.implies_intr_hyps
   val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
- in implies_elim (implies_elim eqI thl) thr |> mk_meta_eq end;
+ in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
 
 fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
 
@@ -136,7 +136,7 @@
                       | _ =>
             conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp 
                  (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx))))
-           |> abstract_rule xn x |> Drule.arg_cong_rule e 
+           |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
            |> Conv.fconv_rule (Conv.arg_conv 
                    (Simplifier.rewrite 
                       (HOL_basic_ss addsimps (simp_thms @ ex_simps))))
@@ -144,7 +144,7 @@
           end
     | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp 
                  (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs))))
-           |> abstract_rule xn x |> Drule.arg_cong_rule e 
+           |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
            |> Conv.fconv_rule (Conv.arg_conv 
                    (Simplifier.rewrite 
                 (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) 
@@ -167,7 +167,7 @@
                 @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib])
  in fn p => 
    Qelim.gen_qelim_conv pcv pcv dnfex_conv cons 
-                  (Thm.add_cterm_frees p [])  (K reflexive) (K reflexive)
+                  (Thm.add_cterm_frees p [])  (K Thm.reflexive) (K Thm.reflexive)
                   (K (basic_dloqe () gst qe_bnds qe_nolb qe_noub gs)) p
  end;
 
@@ -212,7 +212,7 @@
    fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
    val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
    val p' = fold_rev gen ts p
- in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
+ in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
 
 
 fun cfrees ats ct =
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Qelim/qelim.ML
--- a/src/HOL/Tools/Qelim/qelim.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Sat May 15 21:50:05 2010 +0200
@@ -47,7 +47,7 @@
      val p = Thm.dest_arg p
      val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
      val th = instantiate' [SOME T] [SOME p] all_not_ex
-    in transitive th (conv env (Thm.rhs_of th))
+    in Thm.transitive th (conv env (Thm.rhs_of th))
     end
   | _ => atcv env p
  in precv then_conv (conv env) then_conv postcv end
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat May 15 21:50:05 2010 +0200
@@ -517,7 +517,7 @@
 *)
 fun clean_tac lthy =
 let
-  val defs = map (symmetric o #def) (qconsts_dest lthy)
+  val defs = map (Thm.symmetric o #def) (qconsts_dest lthy)
   val prs = prs_rules_get lthy
   val ids = id_simps_get lthy
   val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Sat May 15 21:50:05 2010 +0200
@@ -35,7 +35,7 @@
 (* Useful Theorems                                                           *)
 (* ------------------------------------------------------------------------- *)
 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
-val REFL_THM = incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
+val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
 
@@ -364,7 +364,7 @@
   in  cterm_instantiate substs th  end;
 
 (* INFERENCE RULE: AXIOM *)
-fun axiom_inf thpairs th = incr_indexes 1 (lookth thpairs th);
+fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
     (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
 
 (* INFERENCE RULE: ASSUME *)
@@ -527,7 +527,7 @@
       val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
       val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
       val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
-      val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
+      val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
       val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
       val eq_terms = map (pairself (cterm_of thy))
         (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat May 15 21:50:05 2010 +0200
@@ -209,7 +209,7 @@
                    Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
                  end
             else if loose_bvar1 (rand,0) then (*B or eta*)
-               if rand = Bound 0 then eta_conversion ct
+               if rand = Bound 0 then Thm.eta_conversion ct
                else (*B*)
                  let val crand = cterm_of thy (Abs(x,xT,rand))
                      val crator = cterm_of thy rator
@@ -225,7 +225,7 @@
 (*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
   prefix for the constants.*)
 fun combinators_aux ct =
-  if lambda_free (term_of ct) then reflexive ct
+  if lambda_free (term_of ct) then Thm.reflexive ct
   else
   case term_of ct of
       Abs _ =>
@@ -234,17 +234,17 @@
             val u_th = combinators_aux cta
             val cu = Thm.rhs_of u_th
             val comb_eq = abstract (Thm.cabs cv cu)
-        in transitive (abstract_rule v cv u_th) comb_eq end
+        in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
     | _ $ _ =>
         let val (ct1, ct2) = Thm.dest_comb ct
-        in  combination (combinators_aux ct1) (combinators_aux ct2)  end;
+        in  Thm.combination (combinators_aux ct1) (combinators_aux ct2)  end;
 
 fun combinators th =
   if lambda_free (prop_of th) then th
   else
     let val th = Drule.eta_contraction_rule th
         val eqth = combinators_aux (cprop_of th)
-    in  equal_elim eqth th   end
+    in  Thm.equal_elim eqth th   end
     handle THM (msg,_,_) =>
       (warning (cat_lines
         ["Error in the combinator translation of " ^ Display.string_of_thm_without_context th,
@@ -298,7 +298,7 @@
 
 (*Generate Skolem functions for a theorem supplied in nnf*)
 fun assume_skolem_of_def s th =
-  map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
+  map (skolem_of_def o Thm.assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
 
 
 (*** Blacklisting (FIXME: duplicated in "Sledgehammer_Fact_Filter"?) ***)
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/TFL/casesplit.ML
--- a/src/HOL/Tools/TFL/casesplit.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML	Sat May 15 21:50:05 2010 +0200
@@ -79,8 +79,8 @@
 (* beta-eta contract the theorem *)
 fun beta_eta_contract thm =
     let
-      val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
-      val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
+      val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
+      val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
     in thm3 end;
 
 (* make a casethm from an induction thm *)
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Sat May 15 21:50:05 2010 +0200
@@ -172,7 +172,7 @@
       val [P,Q] = OldTerm.term_vars prop
       val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
 in
-fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
+fun DISJ1 thm tm = thm RS (Thm.forall_elim (D.drop_prop tm) disj1)
   handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
 end;
 
@@ -181,7 +181,7 @@
       val [P,Q] = OldTerm.term_vars prop
       val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
 in
-fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
+fun DISJ2 tm thm = thm RS (Thm.forall_elim (D.drop_prop tm) disj2)
   handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
 end;
 
@@ -276,11 +276,11 @@
       val prop = Thm.prop_of spec
       val x = hd (tl (OldTerm.term_vars prop))
       val cTV = ctyp_of thy (type_of x)
-      val gspec = forall_intr (cterm_of thy x) spec
+      val gspec = Thm.forall_intr (cterm_of thy x) spec
 in
 fun SPEC tm thm =
    let val gspec' = instantiate ([(cTV, Thm.ctyp_of_term tm)], []) gspec
-   in thm RS (forall_elim tm gspec') end
+   in thm RS (Thm.forall_elim tm gspec') end
 end;
 
 fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm;
@@ -302,7 +302,7 @@
          ctm_theta s (Vartab.dest tm_theta))
 in
 fun GEN v th =
-   let val gth = forall_intr v th
+   let val gth = Thm.forall_intr v th
        val thy = Thm.theory_of_thm gth
        val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth
        val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
@@ -533,9 +533,9 @@
  *---------------------------------------------------------------------------*)
 
 fun list_beta_conv tm =
-  let fun rbeta th = Thm.transitive th (beta_conversion false (#2(D.dest_eq(cconcl th))))
+  let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(D.dest_eq(cconcl th))))
       fun iter [] = Thm.reflexive tm
-        | iter (v::rst) = rbeta (combination(iter rst) (Thm.reflexive v))
+        | iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v))
   in iter  end;
 
 
@@ -619,7 +619,7 @@
 fun VSTRUCT_ELIM tych a vstr th =
   let val L = S.free_vars_lr vstr
       val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
-      val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th)
+      val thm1 = Thm.implies_intr bind1 (SUBS [SYM(Thm.assume bind1)] th)
       val thm2 = forall_intr_list (map tych L) thm1
       val thm3 = forall_elim_list (XFILL tych a vstr) thm2
   in refl RS
@@ -630,7 +630,7 @@
   let val a1 = tych a
       val vstr1 = tych vstr
   in
-  forall_intr a1
+  Thm.forall_intr a1
      (if (is_Free vstr)
       then cterm_instantiate [(vstr1,a1)] th
       else VSTRUCT_ELIM tych a vstr th)
@@ -803,7 +803,7 @@
     val names = OldTerm.add_term_names (term_of ctm, [])
     val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
       (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
-    val th2 = equal_elim th1 th
+    val th2 = Thm.equal_elim th1 th
  in
  (th2, filter_out restricted (!tc_list))
  end;
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Sat May 15 21:50:05 2010 +0200
@@ -556,8 +556,8 @@
                            else ()
      val f_free = Free (fid, fastype_of f)  (*'cos f is a Const*)
      val SV' = map tych SV;
-     val SVrefls = map reflexive SV'
-     val def0 = (fold (fn x => fn th => R.rbeta(combination th x))
+     val SVrefls = map Thm.reflexive SV'
+     val def0 = (fold (fn x => fn th => R.rbeta(Thm.combination th x))
                    SVrefls def)
                 RS meta_eq_to_obj_eq
      val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Sat May 15 21:50:05 2010 +0200
@@ -183,7 +183,7 @@
                 fun process_single ((name,atts),rew_imp,frees) args =
                     let
                         fun undo_imps thm =
-                            equal_elim (symmetric rew_imp) thm
+                            Thm.equal_elim (Thm.symmetric rew_imp) thm
 
                         fun add_final (arg as (thy, thm)) =
                             if name = ""
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Sat May 15 21:50:05 2010 +0200
@@ -435,9 +435,9 @@
 					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
 					val var  = new_free ()
 					val thm2 = make_cnfx_disj_thm (betapply (x', var)) y'  (* (x' | y') = body' *)
-					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
-					val thm4 = Thm.strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
-					val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
+					val thm3 = Thm.forall_intr (cterm_of thy var) thm2     (* !!v. (x' | y') = body' *)
+					val thm4 = Thm.strip_shyps (thm3 COMP allI)            (* ALL v. (x' | y') = body' *)
+					val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
 				in
 					iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
 				end
@@ -446,9 +446,9 @@
 					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
 					val var  = new_free ()
 					val thm2 = make_cnfx_disj_thm x' (betapply (y', var))  (* (x' | y') = body' *)
-					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
-					val thm4 = Thm.strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
-					val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
+					val thm3 = Thm.forall_intr (cterm_of thy var) thm2     (* !!v. (x' | y') = body' *)
+					val thm4 = Thm.strip_shyps (thm3 COMP allI)            (* ALL v. (x' | y') = body' *)
+					val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
 				in
 					iff_trans OF [thm1, thm5]  (* (x' | (Ex y')) = (EX v. body') *)
 				end
@@ -466,8 +466,8 @@
 			val var  = new_free ()
 			val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
 			val thm2 = make_cnfx_thm_from_nnf body              (* (x | v) & (y | ~v) = body' *)
-			val thm3 = forall_intr (cterm_of thy var) thm2      (* !!v. (x | v) & (y | ~v) = body' *)
-			val thm4 = Thm.strip_shyps (thm3 COMP allI)             (* ALL v. (x | v) & (y | ~v) = body' *)
+			val thm3 = Thm.forall_intr (cterm_of thy var) thm2  (* !!v. (x | v) & (y | ~v) = body' *)
+			val thm4 = Thm.strip_shyps (thm3 COMP allI)         (* ALL v. (x | v) & (y | ~v) = body' *)
 			val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong)  (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
 		in
 			iff_trans OF [thm1, thm5]
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat May 15 21:50:05 2010 +0200
@@ -21,7 +21,7 @@
     [name] => name
   | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
 
-val all_simps = map (symmetric o mk_meta_eq) @{thms HOL.all_simps};
+val all_simps = map (Thm.symmetric o mk_meta_eq) @{thms HOL.all_simps};
 
 fun prf_of thm =
   let
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Sat May 15 21:50:05 2010 +0200
@@ -114,9 +114,9 @@
             let val rews = map mk_rew ts
             in
               if forall is_none rews then NONE
-              else SOME (fold (fn th1 => fn th2 => combination th2 th1)
-                (map2 (fn SOME r => K r | NONE => reflexive o cterm_of thy)
-                   rews ts) (reflexive (cterm_of thy h)))
+              else SOME (fold (fn th1 => fn th2 => Thm.combination th2 th1)
+                (map2 (fn SOME r => K r | NONE => Thm.reflexive o cterm_of thy)
+                   rews ts) (Thm.reflexive (cterm_of thy h)))
             end
         | NONE => NONE)
       | _ => NONE
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/int_arith.ML	Sat May 15 21:50:05 2010 +0200
@@ -21,7 +21,7 @@
    That is, m and n consist only of 1s combined with "+", "-" and "*".
 *)
 
-val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0};
+val zeroth = (Thm.symmetric o mk_meta_eq) @{thm of_int_0};
 
 val lhss0 = [@{cpat "0::?'a::ring"}];
 
@@ -35,7 +35,7 @@
   make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
   proc = proc0, identifier = []};
 
-val oneth = (symmetric o mk_meta_eq) @{thm of_int_1};
+val oneth = (Thm.symmetric o mk_meta_eq) @{thm of_int_1};
 
 val lhss1 = [@{cpat "1::?'a::ring_1"}];
 
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Sat May 15 21:50:05 2010 +0200
@@ -614,12 +614,12 @@
 
  fun prove_nz ss T t =
     let
-      val z = instantiate_cterm ([(zT,T)],[]) zr
-      val eq = instantiate_cterm ([(eqT,T)],[]) geq
+      val z = Thm.instantiate_cterm ([(zT,T)],[]) zr
+      val eq = Thm.instantiate_cterm ([(eqT,T)],[]) geq
       val th = Simplifier.rewrite (ss addsimps @{thms simp_thms})
            (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
                   (Thm.capply (Thm.capply eq t) z)))
-    in equal_elim (symmetric th) TrueI
+    in Thm.equal_elim (Thm.symmetric th) TrueI
     end
 
  fun proc phi ss ct =
@@ -630,7 +630,7 @@
     val T = ctyp_of_term x
     val [y_nz, z_nz] = map (prove_nz ss T) [y, z]
     val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
-  in SOME (implies_elim (implies_elim th y_nz) z_nz)
+  in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz)
   end
   handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
 
@@ -643,13 +643,13 @@
         let val (x,y) = Thm.dest_binop l val z = r
             val _ = map (HOLogic.dest_number o term_of) [x,y,z]
             val ynz = prove_nz ss T y
-        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
+        in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
         end
      | (_, Const (@{const_name Rings.divide},_)$_$_) =>
         let val (x,y) = Thm.dest_binop r val z = l
             val _ = map (HOLogic.dest_number o term_of) [x,y,z]
             val ynz = prove_nz ss T y
-        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
+        in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
         end
      | _ => NONE)
   end
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/record.ML	Sat May 15 21:50:05 2010 +0200
@@ -2171,7 +2171,7 @@
 
     fun get_upd_acc_congs () =
       let
-        val symdefs = map symmetric (sel_defs @ upd_defs);
+        val symdefs = map Thm.symmetric (sel_defs @ upd_defs);
         val fold_ss = HOL_basic_ss addsimps symdefs;
         val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists;
       in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
@@ -2257,17 +2257,17 @@
         val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l);
         val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r);
         val thl =
-          assume cl                   (*All r. P r*) (* 1 *)
-          |> obj_to_meta_all          (*!!r. P r*)
-          |> equal_elim split_meta'   (*!!n m more. P (ext n m more)*)
-          |> meta_to_obj_all          (*All n m more. P (ext n m more)*) (* 2*)
-          |> implies_intr cl          (* 1 ==> 2 *)
+          Thm.assume cl                   (*All r. P r*) (* 1 *)
+          |> obj_to_meta_all              (*!!r. P r*)
+          |> Thm.equal_elim split_meta'   (*!!n m more. P (ext n m more)*)
+          |> meta_to_obj_all              (*All n m more. P (ext n m more)*) (* 2*)
+          |> Thm.implies_intr cl          (* 1 ==> 2 *)
         val thr =
-          assume cr                             (*All n m more. P (ext n m more)*)
-          |> obj_to_meta_all                    (*!!n m more. P (ext n m more)*)
-          |> equal_elim (symmetric split_meta') (*!!r. P r*)
-          |> meta_to_obj_all                    (*All r. P r*)
-          |> implies_intr cr                    (* 2 ==> 1 *)
+          Thm.assume cr                                 (*All n m more. P (ext n m more)*)
+          |> obj_to_meta_all                            (*!!n m more. P (ext n m more)*)
+          |> Thm.equal_elim (Thm.symmetric split_meta') (*!!r. P r*)
+          |> meta_to_obj_all                            (*All r. P r*)
+          |> Thm.implies_intr cr                        (* 2 ==> 1 *)
      in thr COMP (thl COMP iffI) end;
 
 
diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML	Sat May 15 21:50:05 2010 +0200
@@ -147,7 +147,7 @@
       val semiring = (sr_ops, sr_rules');
       val ring = (r_ops, r_rules');
       val field = (f_ops, f_rules');
-      val ideal' = map (symmetric o mk_meta) ideal
+      val ideal' = map (Thm.symmetric o mk_meta) ideal
     in
       AList.delete Thm.eq_thm key #>
       cons (key, ({vars = vars, semiring = semiring, 
@@ -328,16 +328,16 @@
          ((let val (rx,rn) = dest_pow r
                val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29
                 val (tm1,tm2) = Thm.dest_comb(concl th1) in
-               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
+               Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
            handle CTERM _ =>
             (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31
                  val (tm1,tm2) = Thm.dest_comb(concl th1) in
-               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
+               Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
        handle CTERM _ =>
            ((let val (rx,rn) = dest_pow r
                 val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30
                 val (tm1,tm2) = Thm.dest_comb(concl th1) in
-               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
+               Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
            handle CTERM _ => inst_thm [(cx,l)] pthm_32
 
 ))
@@ -348,7 +348,7 @@
  fun monomial_deone th =
        (let val (l,r) = dest_mul(concl th) in
            if l aconvc one_tm
-          then transitive th (inst_thm [(ca,r)] pthm_13)  else th end)
+          then Thm.transitive th (inst_thm [(ca,r)] pthm_13)  else th end)
        handle CTERM _ => th;
 
 (* Conversion for "(monomial)^n", where n is a numeral.                      *)
@@ -357,7 +357,7 @@
   let
    fun monomial_pow tm bod ntm =
     if not(is_comb bod)
-    then reflexive tm
+    then Thm.reflexive tm
     else
      if is_semiring_constant bod
      then semiring_pow_conv tm
@@ -365,7 +365,7 @@
       let
       val (lopr,r) = Thm.dest_comb bod
       in if not(is_comb lopr)
-         then reflexive tm
+         then Thm.reflexive tm
         else
           let
           val (opr,l) = Thm.dest_comb lopr
@@ -374,7 +374,7 @@
           then
             let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
                 val (l,r) = Thm.dest_comb(concl th1)
-           in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
+           in Thm.transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
            end
            else
             if opr aconvc mul_tm
@@ -385,9 +385,9 @@
               val (x,y) = Thm.dest_comb xy
               val thl = monomial_pow y l ntm
               val thr = monomial_pow z r ntm
-             in transitive th1 (combination (Drule.arg_cong_rule x thl) thr)
+             in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule x thl) thr)
              end
-             else reflexive tm
+             else Thm.reflexive tm
           end
       end
   in fn tm =>
@@ -436,18 +436,18 @@
              val (tm1,tm2) = Thm.dest_comb(concl th1)
              val (tm3,tm4) = Thm.dest_comb tm1
              val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
-             val th3 = transitive th1 th2
+             val th3 = Thm.transitive th1 th2
               val  (tm5,tm6) = Thm.dest_comb(concl th3)
               val  (tm7,tm8) = Thm.dest_comb tm6
              val  th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8
-         in  transitive th3 (Drule.arg_cong_rule tm5 th4)
+         in Thm.transitive th3 (Drule.arg_cong_rule tm5 th4)
          end
          else
           let val th0 = if ord < 0 then pthm_16 else pthm_17
              val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0
              val (tm1,tm2) = Thm.dest_comb(concl th1)
              val (tm3,tm4) = Thm.dest_comb tm2
-         in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
+         in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
          end
         end)
        handle CTERM _ =>
@@ -459,14 +459,14 @@
                  val (tm1,tm2) = Thm.dest_comb(concl th1)
            val (tm3,tm4) = Thm.dest_comb tm1
            val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
-          in transitive th1 th2
+          in Thm.transitive th1 th2
           end
           else
           if ord < 0 then
             let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19
                 val (tm1,tm2) = Thm.dest_comb(concl th1)
                 val (tm3,tm4) = Thm.dest_comb tm2
-           in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
+           in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
            end
            else inst_thm [(ca,l),(cb,r)] pthm_09
         end)) end)
@@ -480,22 +480,22 @@
               let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21
                  val (tm1,tm2) = Thm.dest_comb(concl th1)
                  val (tm3,tm4) = Thm.dest_comb tm1
-             in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
+             in Thm.transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
              end
              else if ord > 0 then
                  let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22
                      val (tm1,tm2) = Thm.dest_comb(concl th1)
                     val (tm3,tm4) = Thm.dest_comb tm2
-                in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
+                in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
                 end
-             else reflexive tm
+             else Thm.reflexive tm
          end)
         handle CTERM _ =>
           (let val vr = powvar r
                val  ord = vorder vl vr
           in if ord = 0 then powvar_mul_conv tm
               else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09
-              else reflexive tm
+              else Thm.reflexive tm
           end)) end))
   in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r)
              end
@@ -511,8 +511,8 @@
           val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37
           val (tm1,tm2) = Thm.dest_comb(concl th1)
           val (tm3,tm4) = Thm.dest_comb tm1
-          val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
-      in transitive th1 th2
+          val th2 = Thm.combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
+      in Thm.transitive th1 th2
       end)
      handle CTERM _ => monomial_mul_conv tm)
    end
@@ -537,11 +537,11 @@
          val (tm1,tm2) = Thm.dest_comb(concl th1)
          val (tm3,tm4) = Thm.dest_comb tm1
          val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4)
-         val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2)
+         val th3 = Thm.transitive th1 (Drule.fun_cong_rule th2 tm2)
          val tm5 = concl th3
       in
       if (Thm.dest_arg1 tm5) aconvc zero_tm
-      then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
+      then Thm.transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
       else monomial_deone th3
      end
  end;
@@ -603,9 +603,9 @@
        val l = Thm.dest_arg lopr
    in
     if l aconvc zero_tm
-    then transitive th (inst_thm [(ca,r)] pthm_07)   else
+    then Thm.transitive th (inst_thm [(ca,r)] pthm_07)   else
         if r aconvc zero_tm
-        then transitive th (inst_thm [(ca,l)] pthm_08)  else th
+        then Thm.transitive th (inst_thm [(ca,l)] pthm_08)  else th
    end
   end
  fun padd tm =
@@ -628,14 +628,14 @@
             val (tm1,tm2) = Thm.dest_comb(concl th1)
             val (tm3,tm4) = Thm.dest_comb tm1
             val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4)
-        in dezero_rule (transitive th1 (combination th2 (padd tm2)))
+        in dezero_rule (Thm.transitive th1 (Thm.combination th2 (padd tm2)))
         end
        else (* ord <> 0*)
         let val th1 =
                 if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
                 else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
             val (tm1,tm2) = Thm.dest_comb(concl th1)
-        in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
+        in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
         end
       end
      else (* not (is_add r)*)
@@ -646,13 +646,13 @@
             val (tm1,tm2) = Thm.dest_comb(concl th1)
             val (tm3,tm4) = Thm.dest_comb tm1
             val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
-        in dezero_rule (transitive th1 th2)
+        in dezero_rule (Thm.transitive th1 th2)
         end
        else (* ord <> 0*)
         if ord > 0 then
           let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
               val (tm1,tm2) = Thm.dest_comb(concl th1)
-          in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
+          in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
           end
         else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
       end
@@ -667,21 +667,21 @@
              val (tm1,tm2) = Thm.dest_comb(concl th1)
              val (tm3,tm4) = Thm.dest_comb tm1
              val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
-         in dezero_rule (transitive th1 th2)
+         in dezero_rule (Thm.transitive th1 th2)
          end
        else
-        if ord > 0 then reflexive tm
+        if ord > 0 then Thm.reflexive tm
         else
          let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
              val (tm1,tm2) = Thm.dest_comb(concl th1)
-         in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
+         in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
          end
       end
     else
      let val ord = morder l r
      in
       if ord = 0 then monomial_add_conv tm
-      else if ord > 0 then dezero_rule(reflexive tm)
+      else if ord > 0 then dezero_rule(Thm.reflexive tm)
       else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
      end
   end
@@ -699,7 +699,7 @@
     else
      if not(is_add r) then
       let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09
-      in transitive th1 (polynomial_monomial_mul_conv(concl th1))
+      in Thm.transitive th1 (polynomial_monomial_mul_conv(concl th1))
       end
      else
        let val (a,b) = dest_add l
@@ -707,8 +707,8 @@
            val (tm1,tm2) = Thm.dest_comb(concl th1)
            val (tm3,tm4) = Thm.dest_comb tm1
            val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4)
-           val th3 = transitive th1 (combination th2 (pmul tm2))
-       in transitive th3 (polynomial_add_conv (concl th3))
+           val th3 = Thm.transitive th1 (Thm.combination th2 (pmul tm2))
+       in Thm.transitive th3 (polynomial_add_conv (concl th3))
        end
    end
  in fn tm =>
@@ -740,9 +740,9 @@
          let val th1 = num_conv n
              val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38
              val (tm1,tm2) = Thm.dest_comb(concl th2)
-             val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
-             val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
-         in transitive th4 (polynomial_mul_conv (concl th4))
+             val th3 = Thm.transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
+             val th4 = Thm.transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
+         in Thm.transitive th4 (polynomial_mul_conv (concl th4))
          end
     end
  in fn tm =>
@@ -755,8 +755,8 @@
    let val (l,r) = Thm.dest_comb tm in
         if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
         let val th1 = inst_thm [(cx',r)] neg_mul
-            val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
-        in transitive th2 (polynomial_monomial_mul_conv (concl th2))
+            val th2 = Thm.transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
+        in Thm.transitive th2 (polynomial_monomial_mul_conv (concl th2))
         end
    end;
 
@@ -767,51 +767,52 @@
       val th1 = inst_thm [(cx',l),(cy',r)] sub_add
       val (tm1,tm2) = Thm.dest_comb(concl th1)
       val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2)
-  in transitive th1 (transitive th2 (polynomial_add_conv (concl th2)))
+  in Thm.transitive th1 (Thm.transitive th2 (polynomial_add_conv (concl th2)))
   end;
 
 (* Conversion from HOL term.                                                 *)
 
 fun polynomial_conv tm =
  if is_semiring_constant tm then semiring_add_conv tm
- else if not(is_comb tm) then reflexive tm
+ else if not(is_comb tm) then Thm.reflexive tm
  else
   let val (lopr,r) = Thm.dest_comb tm
   in if lopr aconvc neg_tm then
        let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
-       in transitive th1 (polynomial_neg_conv (concl th1))
+       in Thm.transitive th1 (polynomial_neg_conv (concl th1))
        end
      else if lopr aconvc inverse_tm then
        let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
-       in transitive th1 (semiring_mul_conv (concl th1))
+       in Thm.transitive th1 (semiring_mul_conv (concl th1))
        end
      else
-       if not(is_comb lopr) then reflexive tm
+       if not(is_comb lopr) then Thm.reflexive tm
        else
          let val (opr,l) = Thm.dest_comb lopr
          in if opr aconvc pow_tm andalso is_numeral r
             then
               let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
-              in transitive th1 (polynomial_pow_conv (concl th1))
+              in Thm.transitive th1 (polynomial_pow_conv (concl th1))
               end
          else if opr aconvc divide_tm 
             then
-              let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) 
+              let val th1 = Thm.combination (Drule.arg_cong_rule opr (polynomial_conv l)) 
                                         (polynomial_conv r)
                   val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv)
                               (Thm.rhs_of th1)
-              in transitive th1 th2
+              in Thm.transitive th1 th2
               end
             else
               if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
               then
-               let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
+               let val th1 =
+                    Thm.combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
                    val f = if opr aconvc add_tm then polynomial_add_conv
                       else if opr aconvc mul_tm then polynomial_mul_conv
                       else polynomial_sub_conv
-               in transitive th1 (f (concl th1))
+               in Thm.transitive th1 (f (concl th1))
                end
-              else reflexive tm
+              else Thm.reflexive tm
          end
   end;
  in
@@ -852,7 +853,7 @@
 
 fun semiring_normalize_ord_conv ctxt ord tm =
   (case match ctxt tm of
-    NONE => reflexive tm
+    NONE => Thm.reflexive tm
   | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
  
 fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
diff -r dbf831a50e4a -r 9bec62c10714 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sat May 15 21:50:05 2010 +0200
@@ -845,8 +845,8 @@
       (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) [neq] of
         SOME spl =>
           let val (ct1, ct2) = extract (cprop_of spl)
-              val thm1 = assume ct1
-              val thm2 = assume ct2
+              val thm1 = Thm.assume ct1
+              val thm2 = Thm.assume ct2
           in Spl (spl, ct1, elim_neq neqs (asms', asms@[thm1]),
             ct2, elim_neq neqs (asms', asms@[thm2]))
           end
@@ -858,8 +858,8 @@
       let
         val (thm1, js1) = fwdproof ss tree1 js
         val (thm2, js2) = fwdproof ss tree2 js1
-        val thm1' = implies_intr ct1 thm1
-        val thm2' = implies_intr ct2 thm2
+        val thm1' = Thm.implies_intr ct1 thm1
+        val thm2' = Thm.implies_intr ct2 thm2
       in (thm2' COMP (thm1' COMP thm), js2) end;
       (* FIXME needs handle THM _ => NONE ? *)
 
@@ -869,11 +869,11 @@
     val thy = ProofContext.theory_of ctxt
     val nTconcl = LA_Logic.neg_prop Tconcl
     val cnTconcl = cterm_of thy nTconcl
-    val nTconclthm = assume cnTconcl
+    val nTconclthm = Thm.assume cnTconcl
     val tree = (if split_neq then splitasms ctxt else Tip) (thms @ [nTconclthm])
     val (Falsethm, _) = fwdproof ss tree js
     val contr = if pos then LA_Logic.ccontr else LA_Logic.notI
-    val concl = implies_intr cnTconcl Falsethm COMP contr
+    val concl = Thm.implies_intr cnTconcl Falsethm COMP contr
   in SOME (trace_thm ctxt "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end
   (*in case concl contains ?-var, which makes assume fail:*)   (* FIXME Variable.import_terms *)
   handle THM _ => NONE;
diff -r dbf831a50e4a -r 9bec62c10714 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/Provers/hypsubst.ML	Sat May 15 21:50:05 2010 +0200
@@ -143,7 +143,7 @@
     [ if inspect_pair bnd false (Data.dest_eq
                                    (Data.dest_Trueprop (#prop (rep_thm th))))
       then th RS Data.eq_reflection
-      else symmetric(th RS Data.eq_reflection) (*reorient*) ]
+      else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
     handle TERM _ => [] | Match => [];
 
 local
diff -r dbf831a50e4a -r 9bec62c10714 src/Tools/Compute_Oracle/compute.ML
--- a/src/Tools/Compute_Oracle/compute.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/Tools/Compute_Oracle/compute.ML	Sat May 15 21:50:05 2010 +0200
@@ -391,9 +391,9 @@
 fun export_thm thy hyps shyps prop =
     let
         val th = export_oracle (thy, hyps, shyps, prop)
-        val hyps = map (fn h => assume (cterm_of thy h)) hyps
+        val hyps = map (fn h => Thm.assume (cterm_of thy h)) hyps
     in
-        fold (fn h => fn p => implies_elim p h) hyps th 
+        fold (fn h => fn p => Thm.implies_elim p h) hyps th 
     end
         
 (* --------- Rewrite ----------- *)
diff -r dbf831a50e4a -r 9bec62c10714 src/Tools/IsaPlanner/rw_inst.ML
--- a/src/Tools/IsaPlanner/rw_inst.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Sat May 15 21:50:05 2010 +0200
@@ -54,13 +54,13 @@
 
 (* beta contract the theorem *)
 fun beta_contract thm = 
-    equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
+    Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
 
 (* beta-eta contract the theorem *)
 fun beta_eta_contract thm = 
     let
-      val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
-      val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
+      val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
+      val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
     in thm3 end;
 
 
diff -r dbf831a50e4a -r 9bec62c10714 src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/Tools/coherent.ML	Sat May 15 21:50:05 2010 +0200
@@ -46,8 +46,8 @@
 fun rulify_elim_conv ct =
   if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct
   else concl_conv (length (Logic.strip_imp_prems (term_of ct)))
-    (rewr_conv (symmetric Data.atomize_elimL) then_conv
-     MetaSimplifier.rewrite true (map symmetric
+    (rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
+     MetaSimplifier.rewrite true (map Thm.symmetric
        [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
 
 end;
diff -r dbf831a50e4a -r 9bec62c10714 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Sat May 15 21:50:05 2010 +0200
@@ -89,7 +89,7 @@
 fun exhaust_induct_tac exh ctxt var i state =
   let
     val thy = ProofContext.theory_of ctxt
-    val (_, _, Bi, _) = dest_state (state, i)
+    val (_, _, Bi, _) = Thm.dest_state (state, i)
     val tn = find_tname var Bi
     val rule =
         if exh then #exhaustion (datatype_info thy tn)