less pervasive names from structure Thm;
authorwenzelm
Sat May 15 21:50:05 2010 +0200 (2010-05-15)
changeset 369459bec62c10714
parent 36944 dbf831a50e4a
child 36946 4eba866311df
less pervasive names from structure Thm;
src/FOLP/simp.ML
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/HOL.thy
src/HOL/Import/import.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Library/reflection.ML
src/HOL/Matrix/cplex/matrixlp.ML
src/HOL/Multivariate_Analysis/normarith.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Prolog/prolog.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Function/context_tree.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Function/pat_completeness.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/ferrante_rackoff.ML
src/HOL/Tools/Qelim/langford.ML
src/HOL/Tools/Qelim/qelim.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/record.ML
src/HOL/Tools/semiring_normalizer.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/hypsubst.ML
src/Tools/Compute_Oracle/compute.ML
src/Tools/IsaPlanner/rw_inst.ML
src/Tools/coherent.ML
src/ZF/Tools/induct_tacs.ML
     1.1 --- a/src/FOLP/simp.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/FOLP/simp.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -431,7 +431,7 @@
     1.4        are represented by rules, generalized over their parameters*)
     1.5  fun add_asms(ss,thm,a,anet,ats,cs) =
     1.6      let val As = strip_varify(nth_subgoal i thm, a, []);
     1.7 -        val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
     1.8 +        val thms = map (Thm.trivial o cterm_of(Thm.theory_of_thm thm)) As;
     1.9          val new_rws = maps mk_rew_rules thms;
    1.10          val rwrls = map mk_trans (maps mk_rew_rules thms);
    1.11          val anet' = fold_rev lhs_insert_thm rwrls anet;
     2.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sat May 15 21:41:32 2010 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sat May 15 21:50:05 2010 +0200
     2.3 @@ -681,7 +681,7 @@
     2.4       else ("Nox",[])
     2.5  | t => if t aconv term_of x then ("x",[]) else ("Nox",[]);
     2.6  
     2.7 -fun xnormalize_conv ctxt [] ct = reflexive ct
     2.8 +fun xnormalize_conv ctxt [] ct = Thm.reflexive ct
     2.9  | xnormalize_conv ctxt (vs as (x::_)) ct =
    2.10     case term_of ct of
    2.11     Const(@{const_name Orderings.less},_)$_$Const(@{const_name Groups.zero},_) =>
    2.12 @@ -696,8 +696,8 @@
    2.13                 (Thm.capply @{cterm "Trueprop"}
    2.14                    (if neg then Thm.capply (Thm.capply clt c) cz
    2.15                      else Thm.capply (Thm.capply clt cz) c))
    2.16 -        val cth = equal_elim (symmetric cthp) TrueI
    2.17 -        val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t])
    2.18 +        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    2.19 +        val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t])
    2.20               (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
    2.21          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    2.22                     (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    2.23 @@ -719,12 +719,12 @@
    2.24                 (Thm.capply @{cterm "Trueprop"}
    2.25                    (if neg then Thm.capply (Thm.capply clt c) cz
    2.26                      else Thm.capply (Thm.capply clt cz) c))
    2.27 -        val cth = equal_elim (symmetric cthp) TrueI
    2.28 -        val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
    2.29 +        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    2.30 +        val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
    2.31               (if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth
    2.32          val rth = th
    2.33        in rth end
    2.34 -    | _ => reflexive ct)
    2.35 +    | _ => Thm.reflexive ct)
    2.36  
    2.37  
    2.38  |  Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Groups.zero},_) =>
    2.39 @@ -740,8 +740,8 @@
    2.40                 (Thm.capply @{cterm "Trueprop"}
    2.41                    (if neg then Thm.capply (Thm.capply clt c) cz
    2.42                      else Thm.capply (Thm.capply clt cz) c))
    2.43 -        val cth = equal_elim (symmetric cthp) TrueI
    2.44 -        val th = implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
    2.45 +        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    2.46 +        val th = Thm.implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
    2.47               (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
    2.48          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    2.49                     (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    2.50 @@ -764,12 +764,12 @@
    2.51                 (Thm.capply @{cterm "Trueprop"}
    2.52                    (if neg then Thm.capply (Thm.capply clt c) cz
    2.53                      else Thm.capply (Thm.capply clt cz) c))
    2.54 -        val cth = equal_elim (symmetric cthp) TrueI
    2.55 -        val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
    2.56 +        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    2.57 +        val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
    2.58               (if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth
    2.59          val rth = th
    2.60        in rth end
    2.61 -    | _ => reflexive ct)
    2.62 +    | _ => Thm.reflexive ct)
    2.63  
    2.64  |  Const("op =",_)$_$Const(@{const_name Groups.zero},_) =>
    2.65     (case whatis x (Thm.dest_arg1 ct) of
    2.66 @@ -782,8 +782,8 @@
    2.67          val cthp = Simplifier.rewrite (simpset_of ctxt)
    2.68              (Thm.capply @{cterm "Trueprop"}
    2.69               (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
    2.70 -        val cth = equal_elim (symmetric cthp) TrueI
    2.71 -        val th = implies_elim
    2.72 +        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    2.73 +        val th = Thm.implies_elim
    2.74                   (instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
    2.75          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    2.76                     (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    2.77 @@ -804,11 +804,11 @@
    2.78          val cthp = Simplifier.rewrite (simpset_of ctxt)
    2.79              (Thm.capply @{cterm "Trueprop"}
    2.80               (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
    2.81 -        val cth = equal_elim (symmetric cthp) TrueI
    2.82 -        val rth = implies_elim
    2.83 +        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    2.84 +        val rth = Thm.implies_elim
    2.85                   (instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
    2.86        in rth end
    2.87 -    | _ => reflexive ct);
    2.88 +    | _ => Thm.reflexive ct);
    2.89  
    2.90  local
    2.91    val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"}
    2.92 @@ -823,7 +823,7 @@
    2.93         val nth = Conv.fconv_rule
    2.94           (Conv.arg_conv (Conv.arg1_conv
    2.95                (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
    2.96 -       val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    2.97 +       val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    2.98     in rth end
    2.99  | Const(@{const_name Orderings.less_eq},_)$a$b =>
   2.100     let val (ca,cb) = Thm.dest_binop ct
   2.101 @@ -832,7 +832,7 @@
   2.102         val nth = Conv.fconv_rule
   2.103           (Conv.arg_conv (Conv.arg1_conv
   2.104                (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
   2.105 -       val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
   2.106 +       val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
   2.107     in rth end
   2.108  
   2.109  | Const("op =",_)$a$b =>
   2.110 @@ -842,10 +842,10 @@
   2.111         val nth = Conv.fconv_rule
   2.112           (Conv.arg_conv (Conv.arg1_conv
   2.113                (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
   2.114 -       val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
   2.115 +       val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
   2.116     in rth end
   2.117  | @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
   2.118 -| _ => reflexive ct
   2.119 +| _ => Thm.reflexive ct
   2.120  end;
   2.121  
   2.122  fun classfield_whatis phi =
     3.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat May 15 21:41:32 2010 +0200
     3.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat May 15 21:50:05 2010 +0200
     3.3 @@ -106,7 +106,7 @@
     3.4        [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
     3.5         TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
     3.6         TRY (simp_tac simpset3 1), TRY (simp_tac cooper_ss 1)]
     3.7 -      (trivial ct))
     3.8 +      (Thm.trivial ct))
     3.9      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    3.10      (* The result of the quantifier elimination *)
    3.11      val (th, tac) = case (prop_of pre_thm) of
     4.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sat May 15 21:41:32 2010 +0200
     4.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sat May 15 21:50:05 2010 +0200
     4.3 @@ -87,7 +87,7 @@
     4.4     val pre_thm = Seq.hd (EVERY
     4.5        [simp_tac simpset0 1,
     4.6         TRY (simp_tac (Simplifier.context ctxt ferrack_ss) 1)]
     4.7 -      (trivial ct))
     4.8 +      (Thm.trivial ct))
     4.9      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    4.10      (* The result of the quantifier elimination *)
    4.11      val (th, tac) = case prop_of pre_thm of
     5.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sat May 15 21:41:32 2010 +0200
     5.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat May 15 21:50:05 2010 +0200
     5.3 @@ -128,7 +128,7 @@
     5.4      val pre_thm = Seq.hd (EVERY
     5.5        [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
     5.6         TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), TRY (simp_tac mir_ss 1)]
     5.7 -      (trivial ct))
     5.8 +      (Thm.trivial ct))
     5.9      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    5.10      (* The result of the quantifier elimination *)
    5.11      val (th, tac) = case (prop_of pre_thm) of
     6.1 --- a/src/HOL/HOL.thy	Sat May 15 21:41:32 2010 +0200
     6.2 +++ b/src/HOL/HOL.thy	Sat May 15 21:50:05 2010 +0200
     6.3 @@ -1282,12 +1282,12 @@
     6.4               else let
     6.5                     val abs_g'= Abs (n,xT,g');
     6.6                     val g'x = abs_g'$x;
     6.7 -                   val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x));
     6.8 +                   val g_g'x = Thm.symmetric (Thm.beta_conversion false (cterm_of thy g'x));
     6.9                     val rl = cterm_instantiate
    6.10                               [(f_Let_folded, cterm_of thy f), (x_Let_folded, cx),
    6.11                                (g_Let_folded, cterm_of thy abs_g')]
    6.12                               @{thm Let_folded};
    6.13 -                 in SOME (rl OF [transitive fx_g g_g'x])
    6.14 +                 in SOME (rl OF [Thm.transitive fx_g g_g'x])
    6.15                   end)
    6.16          end
    6.17      | _ => NONE)
     7.1 --- a/src/HOL/Import/import.ML	Sat May 15 21:41:32 2010 +0200
     7.2 +++ b/src/HOL/Import/import.ML	Sat May 15 21:50:05 2010 +0200
     7.3 @@ -40,7 +40,7 @@
     7.4              val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
     7.5              val thm = snd (ProofKernel.to_isa_thm hol4thm)
     7.6              val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
     7.7 -            val thm = equal_elim rew thm
     7.8 +            val thm = Thm.equal_elim rew thm
     7.9              val prew = ProofKernel.rewrite_hol4_term prem thy
    7.10              val prem' = #2 (Logic.dest_equals (prop_of prew))
    7.11              val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm)
    7.12 @@ -53,7 +53,7 @@
    7.13                      val _ = if prem' aconv (prop_of thm)
    7.14                              then message "import: Terms match up"
    7.15                              else message "import: Terms DO NOT match up"
    7.16 -                    val thm' = equal_elim (symmetric prew) thm
    7.17 +                    val thm' = Thm.equal_elim (Thm.symmetric prew) thm
    7.18                      val res = Thm.bicompose true (false,thm',0) 1 th
    7.19                  in
    7.20                      res
     8.1 --- a/src/HOL/Import/proof_kernel.ML	Sat May 15 21:41:32 2010 +0200
     8.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat May 15 21:50:05 2010 +0200
     8.3 @@ -1013,12 +1013,12 @@
     8.4  local
     8.5      val th = thm "not_def"
     8.6      val thy = theory_of_thm th
     8.7 -    val pp = reflexive (cterm_of thy (Const("Trueprop",boolT-->propT)))
     8.8 +    val pp = Thm.reflexive (cterm_of thy (Const("Trueprop",boolT-->propT)))
     8.9  in
    8.10 -val not_elim_thm = combination pp th
    8.11 +val not_elim_thm = Thm.combination pp th
    8.12  end
    8.13  
    8.14 -val not_intro_thm = symmetric not_elim_thm
    8.15 +val not_intro_thm = Thm.symmetric not_elim_thm
    8.16  val abs_thm = thm "ext"
    8.17  val trans_thm = thm "trans"
    8.18  val symmetry_thm = thm "sym"
    8.19 @@ -1039,7 +1039,7 @@
    8.20      end
    8.21  
    8.22  fun implies_elim_all th =
    8.23 -    Library.foldl (fn (th,p) => implies_elim th (assume p)) (th,cprems_of th)
    8.24 +    Library.foldl (fn (th,p) => Thm.implies_elim th (Thm.assume p)) (th,cprems_of th)
    8.25  
    8.26  fun norm_hyps th =
    8.27      th |> beta_eta_thm
    8.28 @@ -1054,7 +1054,7 @@
    8.29          val clc = Thm.cterm_of sg lc
    8.30          val cvty = ctyp_of_term cv
    8.31          val th1 = implies_elim_all th
    8.32 -        val th2 = beta_eta_thm (forall_intr cv th1)
    8.33 +        val th2 = beta_eta_thm (Thm.forall_intr cv th1)
    8.34          val th3 = th2 COMP (beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME clc] gen_thm))
    8.35          val c = prop_of th3
    8.36          val vname = fst(dest_Free v)
    8.37 @@ -1072,7 +1072,7 @@
    8.38  fun rearrange sg tm th =
    8.39      let
    8.40          val tm' = Envir.beta_eta_contract tm
    8.41 -        fun find []      n = Thm.permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
    8.42 +        fun find []      n = Thm.permute_prems 0 1 (Thm.implies_intr (Thm.cterm_of sg tm) th)
    8.43            | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p)
    8.44                               then Thm.permute_prems n 1 th
    8.45                               else find ps (n+1)
    8.46 @@ -1258,7 +1258,7 @@
    8.47  fun get_isabelle_thm thyname thmname hol4conc thy =
    8.48      let
    8.49          val (info,hol4conc') = disamb_term hol4conc
    8.50 -        val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
    8.51 +        val i2h_conc = Thm.symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
    8.52          val isaconc =
    8.53              case concl_of i2h_conc of
    8.54                  Const("==",_) $ lhs $ _ => lhs
    8.55 @@ -1268,7 +1268,7 @@
    8.56                   message "Modified conclusion:";
    8.57                   if_debug prin isaconc)
    8.58  
    8.59 -        fun mk_res th = HOLThm(rens_of info,equal_elim i2h_conc th)
    8.60 +        fun mk_res th = HOLThm (rens_of info, Thm.equal_elim i2h_conc th)
    8.61      in
    8.62          case get_hol4_mapping thyname thmname thy of
    8.63              SOME (SOME thmname) =>
    8.64 @@ -1320,7 +1320,7 @@
    8.65      fun warn () =
    8.66          let
    8.67              val (info,hol4conc') = disamb_term hol4conc
    8.68 -            val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
    8.69 +            val i2h_conc = Thm.symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
    8.70          in
    8.71              case concl_of i2h_conc of
    8.72                  Const("==",_) $ lhs $ _ =>
    8.73 @@ -1369,7 +1369,7 @@
    8.74      let
    8.75          val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth
    8.76          val rew = rewrite_hol4_term (concl_of th) thy
    8.77 -        val th  = equal_elim rew th
    8.78 +        val th  = Thm.equal_elim rew th
    8.79          val thy' = add_hol4_pending thyname thmname args thy
    8.80          val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
    8.81          val th = disambiguate_frees th
    8.82 @@ -1683,7 +1683,7 @@
    8.83          val (info',v') = disamb_term_from info v
    8.84          fun strip 0 _ th = th
    8.85            | strip n (p::ps) th =
    8.86 -            strip (n-1) ps (implies_elim th (assume p))
    8.87 +            strip (n-1) ps (Thm.implies_elim th (Thm.assume p))
    8.88            | strip _ _ _ = raise ERR "CHOOSE" "strip error"
    8.89          val cv = cterm_of thy v'
    8.90          val th2 = norm_hyps th2
    8.91 @@ -1697,7 +1697,7 @@
    8.92          val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
    8.93          val th21 = rearrange thy (HOLogic.mk_Trueprop (a $ v')) th2
    8.94          val th22 = strip ((nprems_of th21)-1) (cprems_of th21) th21
    8.95 -        val th23 = beta_eta_thm (forall_intr cv th22)
    8.96 +        val th23 = beta_eta_thm (Thm.forall_intr cv th22)
    8.97          val th11 = implies_elim_all (beta_eta_thm th1)
    8.98          val th' = th23 COMP (th11 COMP choose_thm')
    8.99          val th = implies_intr_hyps th'
   8.100 @@ -1796,7 +1796,7 @@
   8.101                        | _ => raise ERR "mk_ABS" "Bad conclusion"
   8.102          val (fd,fr) = dom_rng (type_of f)
   8.103          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
   8.104 -        val th2 = forall_intr cv th1
   8.105 +        val th2 = Thm.forall_intr cv th1
   8.106          val th3 = th2 COMP abs_thm'
   8.107          val res = implies_intr_hyps th3
   8.108      in
   8.109 @@ -1867,7 +1867,7 @@
   8.110                      _ $ (Const("op -->",_) $ a $ Const("False",_)) => a
   8.111                    | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
   8.112          val ca = cterm_of thy a
   8.113 -        val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
   8.114 +        val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
   8.115          val res = HOLThm(rens,implies_intr_hyps th2)
   8.116          val _ = message "RESULT:"
   8.117          val _ = if_debug pth res
   8.118 @@ -1884,7 +1884,7 @@
   8.119                      _ $ (Const("Not",_) $ a) => a
   8.120                    | _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
   8.121          val ca = cterm_of thy a
   8.122 -        val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
   8.123 +        val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
   8.124          val res = HOLThm(rens,implies_intr_hyps th2)
   8.125          val _ = message "RESULT:"
   8.126          val _ = if_debug pth res
   8.127 @@ -1902,9 +1902,9 @@
   8.128          val prems = prems_of th
   8.129          val th1 = beta_eta_thm th
   8.130          val th2 = implies_elim_all th1
   8.131 -        val th3 = implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2
   8.132 +        val th3 = Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2
   8.133          val th4 = th3 COMP disch_thm
   8.134 -        val res = HOLThm(rens_of info',implies_intr_hyps th4)
   8.135 +        val res = HOLThm (rens_of info', implies_intr_hyps th4)
   8.136          val _ = message "RESULT:"
   8.137          val _ = if_debug pth res
   8.138      in
   8.139 @@ -2032,7 +2032,7 @@
   8.140              val res' = Thm.unvarify_global res
   8.141              val hth = HOLThm(rens,res')
   8.142              val rew = rewrite_hol4_term (concl_of res') thy'
   8.143 -            val th  = equal_elim rew res'
   8.144 +            val th  = Thm.equal_elim rew res'
   8.145              fun handle_const (name,thy) =
   8.146                  let
   8.147                      val defname = Thm.def_name name
   8.148 @@ -2112,7 +2112,7 @@
   8.149              val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
   8.150  
   8.151              val rew = rewrite_hol4_term (concl_of td_th) thy4
   8.152 -            val th  = equal_elim rew (Thm.transfer thy4 td_th)
   8.153 +            val th  = Thm.equal_elim rew (Thm.transfer thy4 td_th)
   8.154              val c   = case HOLogic.dest_Trueprop (prop_of th) of
   8.155                            Const("Ex",exT) $ P =>
   8.156                            let
     9.1 --- a/src/HOL/Import/shuffler.ML	Sat May 15 21:41:32 2010 +0200
     9.2 +++ b/src/HOL/Import/shuffler.ML	Sat May 15 21:50:05 2010 +0200
     9.3 @@ -95,12 +95,12 @@
     9.4          val cQ = cert Q
     9.5          val cPQ = cert PQ
     9.6          val cPPQ = cert PPQ
     9.7 -        val th1 = assume cPQ |> implies_intr_list [cPQ,cP]
     9.8 -        val th3 = assume cP
     9.9 -        val th4 = implies_elim_list (assume cPPQ) [th3,th3]
    9.10 +        val th1 = Thm.assume cPQ |> implies_intr_list [cPQ,cP]
    9.11 +        val th3 = Thm.assume cP
    9.12 +        val th4 = implies_elim_list (Thm.assume cPPQ) [th3,th3]
    9.13                                      |> implies_intr_list [cPPQ,cP]
    9.14      in
    9.15 -        equal_intr th4 th1 |> Drule.export_without_context
    9.16 +        Thm.equal_intr th4 th1 |> Drule.export_without_context
    9.17      end
    9.18  
    9.19  val imp_comm =
    9.20 @@ -115,12 +115,12 @@
    9.21          val cQ = cert Q
    9.22          val cPQR = cert PQR
    9.23          val cQPR = cert QPR
    9.24 -        val th1 = implies_elim_list (assume cPQR) [assume cP,assume cQ]
    9.25 +        val th1 = implies_elim_list (Thm.assume cPQR) [Thm.assume cP,Thm.assume cQ]
    9.26                                      |> implies_intr_list [cPQR,cQ,cP]
    9.27 -        val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP]
    9.28 +        val th2 = implies_elim_list (Thm.assume cQPR) [Thm.assume cQ,Thm.assume cP]
    9.29                                      |> implies_intr_list [cQPR,cP,cQ]
    9.30      in
    9.31 -        equal_intr th1 th2 |> Drule.export_without_context
    9.32 +        Thm.equal_intr th1 th2 |> Drule.export_without_context
    9.33      end
    9.34  
    9.35  val def_norm =
    9.36 @@ -134,20 +134,20 @@
    9.37          val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0)))
    9.38          val cPQ = cert (Logic.mk_equals(P,Q))
    9.39          val cv = cert v
    9.40 -        val rew = assume cvPQ
    9.41 -                         |> forall_elim cv
    9.42 -                         |> abstract_rule "v" cv
    9.43 +        val rew = Thm.assume cvPQ
    9.44 +                         |> Thm.forall_elim cv
    9.45 +                         |> Thm.abstract_rule "v" cv
    9.46          val (lhs,rhs) = Logic.dest_equals(concl_of rew)
    9.47 -        val th1 = transitive (transitive
    9.48 -                                  (eta_conversion (cert lhs) |> symmetric)
    9.49 +        val th1 = Thm.transitive (Thm.transitive
    9.50 +                                  (Thm.eta_conversion (cert lhs) |> Thm.symmetric)
    9.51                                    rew)
    9.52 -                             (eta_conversion (cert rhs))
    9.53 -                             |> implies_intr cvPQ
    9.54 -        val th2 = combination (assume cPQ) (reflexive cv)
    9.55 -                              |> forall_intr cv
    9.56 -                              |> implies_intr cPQ
    9.57 +                             (Thm.eta_conversion (cert rhs))
    9.58 +                             |> Thm.implies_intr cvPQ
    9.59 +        val th2 = Thm.combination (Thm.assume cPQ) (Thm.reflexive cv)
    9.60 +                              |> Thm.forall_intr cv
    9.61 +                              |> Thm.implies_intr cPQ
    9.62      in
    9.63 -        equal_intr th1 th2 |> Drule.export_without_context
    9.64 +        Thm.equal_intr th1 th2 |> Drule.export_without_context
    9.65      end
    9.66  
    9.67  val all_comm =
    9.68 @@ -164,16 +164,16 @@
    9.69          val cr = cert rhs
    9.70          val cx = cert x
    9.71          val cy = cert y
    9.72 -        val th1 = assume cr
    9.73 +        val th1 = Thm.assume cr
    9.74                           |> forall_elim_list [cy,cx]
    9.75                           |> forall_intr_list [cx,cy]
    9.76 -                         |> implies_intr cr
    9.77 -        val th2 = assume cl
    9.78 +                         |> Thm.implies_intr cr
    9.79 +        val th2 = Thm.assume cl
    9.80                           |> forall_elim_list [cx,cy]
    9.81                           |> forall_intr_list [cy,cx]
    9.82 -                         |> implies_intr cl
    9.83 +                         |> Thm.implies_intr cl
    9.84      in
    9.85 -        equal_intr th1 th2 |> Drule.export_without_context
    9.86 +        Thm.equal_intr th1 th2 |> Drule.export_without_context
    9.87      end
    9.88  
    9.89  val equiv_comm =
    9.90 @@ -184,10 +184,10 @@
    9.91          val u    = Free("u",T)
    9.92          val ctu  = cert (Logic.mk_equals(t,u))
    9.93          val cut  = cert (Logic.mk_equals(u,t))
    9.94 -        val th1  = assume ctu |> symmetric |> implies_intr ctu
    9.95 -        val th2  = assume cut |> symmetric |> implies_intr cut
    9.96 +        val th1  = Thm.assume ctu |> Thm.symmetric |> Thm.implies_intr ctu
    9.97 +        val th2  = Thm.assume cut |> Thm.symmetric |> Thm.implies_intr cut
    9.98      in
    9.99 -        equal_intr th1 th2 |> Drule.export_without_context
   9.100 +        Thm.equal_intr th1 th2 |> Drule.export_without_context
   9.101      end
   9.102  
   9.103  (* This simplification procedure rewrites !!x y. P x y
   9.104 @@ -217,7 +217,7 @@
   9.105          val lhs = list_all ([xv,yv],t)
   9.106          val rhs = list_all ([yv,xv],swap_bound 0 t)
   9.107          val rew = Logic.mk_equals (lhs,rhs)
   9.108 -        val init = trivial (cterm_of thy rew)
   9.109 +        val init = Thm.trivial (cterm_of thy rew)
   9.110      in
   9.111          (all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
   9.112      end
   9.113 @@ -232,10 +232,10 @@
   9.114                   then
   9.115                       let
   9.116                           val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body)))
   9.117 -                         val t_th    = reflexive (cterm_of thy t)
   9.118 -                         val newt_th = reflexive (cterm_of thy newt)
   9.119 +                         val t_th    = Thm.reflexive (cterm_of thy t)
   9.120 +                         val newt_th = Thm.reflexive (cterm_of thy newt)
   9.121                       in
   9.122 -                         SOME (transitive t_th newt_th)
   9.123 +                         SOME (Thm.transitive t_th newt_th)
   9.124                       end
   9.125                   else NONE
   9.126            | _ => error "norm_term (quant_rewrite) internal error"
   9.127 @@ -294,7 +294,7 @@
   9.128  fun eta_contract thy assumes origt =
   9.129      let
   9.130          val (typet,Tinst) = freeze_thaw_term origt
   9.131 -        val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet))
   9.132 +        val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet))
   9.133          val final = inst_tfrees thy Tinst o thaw
   9.134          val t = #1 (Logic.dest_equals (prop_of init))
   9.135          val _ =
   9.136 @@ -322,18 +322,18 @@
   9.137                        val v = Free (Name.variant (Term.add_free_names t []) "v", xT)
   9.138                        val cv = cert v
   9.139                        val ct = cert t
   9.140 -                      val th = (assume ct)
   9.141 -                                   |> forall_elim cv
   9.142 -                                   |> abstract_rule x cv
   9.143 -                      val ext_th = eta_conversion (cert (Abs(x,xT,P)))
   9.144 -                      val th' = transitive (symmetric ext_th) th
   9.145 +                      val th = (Thm.assume ct)
   9.146 +                                   |> Thm.forall_elim cv
   9.147 +                                   |> Thm.abstract_rule x cv
   9.148 +                      val ext_th = Thm.eta_conversion (cert (Abs(x,xT,P)))
   9.149 +                      val th' = Thm.transitive (Thm.symmetric ext_th) th
   9.150                        val cu = cert (prop_of th')
   9.151 -                      val uth = combination (assume cu) (reflexive cv)
   9.152 -                      val uth' = (beta_conversion false (cert (Abs(x,xT,Q) $ v)))
   9.153 -                                     |> transitive uth
   9.154 -                                     |> forall_intr cv
   9.155 -                                     |> implies_intr cu
   9.156 -                      val rew_th = equal_intr (th' |> implies_intr ct) uth'
   9.157 +                      val uth = Thm.combination (Thm.assume cu) (Thm.reflexive cv)
   9.158 +                      val uth' = (Thm.beta_conversion false (cert (Abs(x,xT,Q) $ v)))
   9.159 +                                     |> Thm.transitive uth
   9.160 +                                     |> Thm.forall_intr cv
   9.161 +                                     |> Thm.implies_intr cu
   9.162 +                      val rew_th = Thm.equal_intr (th' |> Thm.implies_intr ct) uth'
   9.163                        val res = final rew_th
   9.164                        val lhs = (#1 (Logic.dest_equals (prop_of res)))
   9.165                    in
   9.166 @@ -345,7 +345,7 @@
   9.167         end
   9.168  
   9.169  fun beta_fun thy assume t =
   9.170 -    SOME (beta_conversion true (cterm_of thy t))
   9.171 +    SOME (Thm.beta_conversion true (cterm_of thy t))
   9.172  
   9.173  val meta_sym_rew = thm "refl"
   9.174  
   9.175 @@ -357,7 +357,7 @@
   9.176  fun eta_expand thy assumes origt =
   9.177      let
   9.178          val (typet,Tinst) = freeze_thaw_term origt
   9.179 -        val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet))
   9.180 +        val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet))
   9.181          val final = inst_tfrees thy Tinst o thaw
   9.182          val t = #1 (Logic.dest_equals (prop_of init))
   9.183          val _ =
   9.184 @@ -387,20 +387,20 @@
   9.185                            val v = Free(vname,aT)
   9.186                            val cv = cert v
   9.187                            val ct = cert t
   9.188 -                          val th1 = (combination (assume ct) (reflexive cv))
   9.189 -                                        |> forall_intr cv
   9.190 -                                        |> implies_intr ct
   9.191 +                          val th1 = (Thm.combination (Thm.assume ct) (Thm.reflexive cv))
   9.192 +                                        |> Thm.forall_intr cv
   9.193 +                                        |> Thm.implies_intr ct
   9.194                            val concl = cert (concl_of th1)
   9.195 -                          val th2 = (assume concl)
   9.196 -                                        |> forall_elim cv
   9.197 -                                        |> abstract_rule vname cv
   9.198 +                          val th2 = (Thm.assume concl)
   9.199 +                                        |> Thm.forall_elim cv
   9.200 +                                        |> Thm.abstract_rule vname cv
   9.201                            val (lhs,rhs) = Logic.dest_equals (prop_of th2)
   9.202 -                          val elhs = eta_conversion (cert lhs)
   9.203 -                          val erhs = eta_conversion (cert rhs)
   9.204 -                          val th2' = transitive
   9.205 -                                         (transitive (symmetric elhs) th2)
   9.206 +                          val elhs = Thm.eta_conversion (cert lhs)
   9.207 +                          val erhs = Thm.eta_conversion (cert rhs)
   9.208 +                          val th2' = Thm.transitive
   9.209 +                                         (Thm.transitive (Thm.symmetric elhs) th2)
   9.210                                           erhs
   9.211 -                          val res = equal_intr th1 (th2' |> implies_intr concl)
   9.212 +                          val res = Thm.equal_intr th1 (th2' |> Thm.implies_intr concl)
   9.213                            val res' = final res
   9.214                        in
   9.215                            SOME res'
   9.216 @@ -475,7 +475,7 @@
   9.217          val (t',_) = F (t,0)
   9.218          val ct = cterm_of thy t
   9.219          val ct' = cterm_of thy t'
   9.220 -        val res = transitive (reflexive ct) (reflexive ct')
   9.221 +        val res = Thm.transitive (Thm.reflexive ct) (Thm.reflexive ct')
   9.222          val _ = message ("disamb_term: " ^ (string_of_thm res))
   9.223      in
   9.224          res
   9.225 @@ -496,12 +496,12 @@
   9.226              let
   9.227                  val rhs = Thm.rhs_of th
   9.228              in
   9.229 -                transitive th (f rhs)
   9.230 +                Thm.transitive th (f rhs)
   9.231              end
   9.232          val th =
   9.233              t |> disamb_bound thy
   9.234                |> chain (Simplifier.full_rewrite ss)
   9.235 -              |> chain eta_conversion
   9.236 +              |> chain Thm.eta_conversion
   9.237                |> Thm.strip_shyps
   9.238          val _ = message ("norm_term: " ^ (string_of_thm th))
   9.239      in
   9.240 @@ -529,7 +529,7 @@
   9.241      let
   9.242          val c = prop_of th
   9.243      in
   9.244 -        equal_elim (norm_term thy c) th
   9.245 +        Thm.equal_elim (norm_term thy c) th
   9.246      end
   9.247  
   9.248  (* make_equal thy t u tries to construct the theorem t == u under the
   9.249 @@ -540,7 +540,7 @@
   9.250      let
   9.251          val t_is_t' = norm_term thy t
   9.252          val u_is_u' = norm_term thy u
   9.253 -        val th = transitive t_is_t' (symmetric u_is_u')
   9.254 +        val th = Thm.transitive t_is_t' (Thm.symmetric u_is_u')
   9.255          val _ = message ("make_equal: SOME " ^ (string_of_thm th))
   9.256      in
   9.257          SOME th
   9.258 @@ -593,7 +593,7 @@
   9.259            | process ((name,th)::thms) =
   9.260              let
   9.261                  val norm_th = Thm.varifyT_global (norm_thm thy (close_thm (Thm.transfer thy th)))
   9.262 -                val triv_th = trivial rhs
   9.263 +                val triv_th = Thm.trivial rhs
   9.264                  val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
   9.265                  val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
   9.266                                   SOME(th,_) => SOME th
   9.267 @@ -602,7 +602,7 @@
   9.268                  case mod_th of
   9.269                      SOME mod_th =>
   9.270                      let
   9.271 -                        val closed_th = equal_elim (symmetric rew_th) mod_th
   9.272 +                        val closed_th = Thm.equal_elim (Thm.symmetric rew_th) mod_th
   9.273                      in
   9.274                          message ("Shuffler.set_prop succeeded by " ^ name);
   9.275                          SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th)
    10.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Sat May 15 21:41:32 2010 +0200
    10.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Sat May 15 21:50:05 2010 +0200
    10.3 @@ -1272,7 +1272,7 @@
    10.4  fun subst_conv eqs t =
    10.5   let
    10.6    val t' = fold (Thm.cabs o Thm.lhs_of) eqs t
    10.7 - in Conv.fconv_rule (Thm.beta_conversion true) (fold (C combination) eqs (reflexive t'))
    10.8 + in Conv.fconv_rule (Thm.beta_conversion true) (fold (C Thm.combination) eqs (Thm.reflexive t'))
    10.9   end
   10.10  
   10.11  (* A wrapper that tries to substitute away variables first.                  *)
    11.1 --- a/src/HOL/Library/positivstellensatz.ML	Sat May 15 21:41:32 2010 +0200
    11.2 +++ b/src/HOL/Library/positivstellensatz.ML	Sat May 15 21:50:05 2010 +0200
    11.3 @@ -182,12 +182,12 @@
    11.4  
    11.5      (* Some useful derived rules *)
    11.6  fun deduct_antisym_rule tha thb = 
    11.7 -    equal_intr (implies_intr (cprop_of thb) tha) 
    11.8 -     (implies_intr (cprop_of tha) thb);
    11.9 +    Thm.equal_intr (Thm.implies_intr (cprop_of thb) tha) 
   11.10 +     (Thm.implies_intr (cprop_of tha) thb);
   11.11  
   11.12  fun prove_hyp tha thb = 
   11.13    if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb)) 
   11.14 -  then equal_elim (symmetric (deduct_antisym_rule tha thb)) tha else thb;
   11.15 +  then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb;
   11.16  
   11.17  val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and
   11.18       "((x = y) == (x - y = 0))" and "((~(x < y)) == (x - y >= 0))" and
   11.19 @@ -375,7 +375,7 @@
   11.20   val skolemize_conv = Simplifier.rewrite (Simplifier.context ctxt skolemize_ss)
   11.21   val weak_dnf_ss = HOL_basic_ss addsimps weak_dnf_simps
   11.22   val weak_dnf_conv = Simplifier.rewrite (Simplifier.context ctxt weak_dnf_ss)
   11.23 - fun eqT_elim th = equal_elim (symmetric th) @{thm TrueI}
   11.24 + fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI}
   11.25   fun oprconv cv ct = 
   11.26    let val g = Thm.dest_fun2 ct
   11.27    in if g aconvc @{cterm "op <= :: real => _"} 
   11.28 @@ -387,7 +387,7 @@
   11.29    let
   11.30     val th' = (Thm.instantiate (Thm.match (Thm.lhs_of th, ct)) th 
   11.31        handle MATCH => raise CTERM ("real_ineq_conv", [ct]))
   11.32 -  in transitive th' (oprconv poly_conv (Thm.rhs_of th'))
   11.33 +  in Thm.transitive th' (oprconv poly_conv (Thm.rhs_of th'))
   11.34    end 
   11.35    val [real_lt_conv, real_le_conv, real_eq_conv,
   11.36         real_not_lt_conv, real_not_le_conv, _] =
   11.37 @@ -446,10 +446,10 @@
   11.38     let val (p,q) = Thm.dest_binop (concl th)
   11.39         val c = concl th1
   11.40         val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible"
   11.41 -   in implies_elim (implies_elim
   11.42 -          (implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
   11.43 -          (implies_intr (Thm.capply @{cterm Trueprop} p) th1))
   11.44 -        (implies_intr (Thm.capply @{cterm Trueprop} q) th2)
   11.45 +   in Thm.implies_elim (Thm.implies_elim
   11.46 +          (Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
   11.47 +          (Thm.implies_intr (Thm.capply @{cterm Trueprop} p) th1))
   11.48 +        (Thm.implies_intr (Thm.capply @{cterm Trueprop} q) th2)
   11.49     end
   11.50   fun overall cert_choice dun ths = case ths of
   11.51    [] =>
   11.52 @@ -468,8 +468,8 @@
   11.53        overall cert_choice dun (th1::th2::oths) end
   11.54      else if is_disj ct then
   11.55        let 
   11.56 -       val (th1, cert1) = overall (Left::cert_choice) dun (assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
   11.57 -       val (th2, cert2) = overall (Right::cert_choice) dun (assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
   11.58 +       val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
   11.59 +       val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
   11.60        in (disj_cases th th1 th2, Branch (cert1, cert2)) end
   11.61     else overall cert_choice (th::dun) oths
   11.62    end
   11.63 @@ -487,12 +487,12 @@
   11.64      val th' = Drule.binop_cong_rule @{cterm "op |"} 
   11.65       (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
   11.66       (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
   11.67 -    in transitive th th' 
   11.68 +    in Thm.transitive th th' 
   11.69    end
   11.70   fun equal_implies_1_rule PQ = 
   11.71    let 
   11.72     val P = Thm.lhs_of PQ
   11.73 -  in implies_intr P (equal_elim PQ (assume P))
   11.74 +  in Thm.implies_intr P (Thm.equal_elim PQ (Thm.assume P))
   11.75    end
   11.76   (* FIXME!!! Copied from groebner.ml *)
   11.77   val strip_exists =
   11.78 @@ -507,7 +507,7 @@
   11.79   | Var ((s,_),_) => s
   11.80   | _ => "x"
   11.81  
   11.82 -  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)
   11.83 +  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)
   11.84  
   11.85    val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
   11.86  
   11.87 @@ -523,12 +523,12 @@
   11.88           (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
   11.89       val pv = (Thm.rhs_of o Thm.beta_conversion true) 
   11.90             (Thm.capply @{cterm Trueprop} (Thm.capply p v))
   11.91 -     val th1 = forall_intr v (implies_intr pv th')
   11.92 -    in implies_elim (implies_elim th0 th) th1  end
   11.93 +     val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
   11.94 +    in Thm.implies_elim (Thm.implies_elim th0 th) th1  end
   11.95   | _ => raise THM ("choose",0,[th, th'])
   11.96  
   11.97    fun simple_choose v th = 
   11.98 -     choose v (assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
   11.99 +     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
  11.100  
  11.101   val strip_forall =
  11.102    let fun h (acc, t) =
  11.103 @@ -558,11 +558,11 @@
  11.104      val (evs,bod) = strip_exists tm0
  11.105      val (avs,ibod) = strip_forall bod
  11.106      val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
  11.107 -    val (th2, certs) = overall [] [] [specl avs (assume (Thm.rhs_of th1))]
  11.108 -    val th3 = fold simple_choose evs (prove_hyp (equal_elim th1 (assume (Thm.capply @{cterm Trueprop} bod))) th2)
  11.109 -   in (Drule.implies_intr_hyps (prove_hyp (equal_elim th0 (assume nct)) th3), certs)
  11.110 +    val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))]
  11.111 +    val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.capply @{cterm Trueprop} bod))) th2)
  11.112 +   in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
  11.113     end
  11.114 -  in (implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
  11.115 +  in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
  11.116   end
  11.117  in f
  11.118  end;
  11.119 @@ -715,10 +715,10 @@
  11.120     fun eliminate_construct p c tm =
  11.121      let 
  11.122       val t = find_cterm p tm
  11.123 -     val th0 = (symmetric o beta_conversion false) (Thm.capply (Thm.cabs t tm) t)
  11.124 +     val th0 = (Thm.symmetric o Thm.beta_conversion false) (Thm.capply (Thm.cabs t tm) t)
  11.125       val (p,ax) = (Thm.dest_comb o Thm.rhs_of) th0
  11.126 -    in fconv_rule(arg_conv(binop_conv (arg_conv (beta_conversion false))))
  11.127 -               (transitive th0 (c p ax))
  11.128 +    in fconv_rule(arg_conv(binop_conv (arg_conv (Thm.beta_conversion false))))
  11.129 +               (Thm.transitive th0 (c p ax))
  11.130     end
  11.131  
  11.132     val elim_abs = eliminate_construct is_abs
    12.1 --- a/src/HOL/Library/reflection.ML	Sat May 15 21:41:32 2010 +0200
    12.2 +++ b/src/HOL/Library/reflection.ML	Sat May 15 21:50:05 2010 +0200
    12.3 @@ -133,7 +133,7 @@
    12.4                               (AList.update Type.could_unify (HOLogic.listT xT, ((x::bsT), atsT)) bds))
    12.5                 in (([(ta, ctxt')],
    12.6                      fn ([th], bds) =>
    12.7 -                      (hd (Variable.export ctxt' ctxt [(forall_intr (cert x) th) COMP allI]),
    12.8 +                      (hd (Variable.export ctxt' ctxt [(Thm.forall_intr (cert x) th) COMP allI]),
    12.9                         let val (bsT,asT) = the(AList.lookup Type.could_unify bds (HOLogic.listT xT))
   12.10                         in AList.update Type.could_unify (HOLogic.listT xT,(tl bsT,asT)) bds
   12.11                         end)),
    13.1 --- a/src/HOL/Matrix/cplex/matrixlp.ML	Sat May 15 21:41:32 2010 +0200
    13.2 +++ b/src/HOL/Matrix/cplex/matrixlp.ML	Sat May 15 21:50:05 2010 +0200
    13.3 @@ -81,8 +81,8 @@
    13.4  fun matrix_simplify th =
    13.5      let
    13.6          val simp_th = matrix_compute (cprop_of th)
    13.7 -        val th = Thm.strip_shyps (equal_elim simp_th th)
    13.8 -        fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th  (* FIXME avoid handle _ *)
    13.9 +        val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
   13.10 +        fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle _ => th  (* FIXME avoid handle _ *)
   13.11      in
   13.12          removeTrue th
   13.13      end
    14.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Sat May 15 21:41:32 2010 +0200
    14.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Sat May 15 21:50:05 2010 +0200
    14.3 @@ -80,8 +80,8 @@
    14.4  fun replacenegnorms cv t = case term_of t of
    14.5    @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
    14.6  | @{term "op * :: real => _"}$_$_ =>
    14.7 -    if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else reflexive t
    14.8 -| _ => reflexive t
    14.9 +    if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else Thm.reflexive t
   14.10 +| _ => Thm.reflexive t
   14.11  fun flip v eq =
   14.12    if FuncUtil.Ctermfunc.defined eq v
   14.13    then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq
   14.14 @@ -211,7 +211,7 @@
   14.15                  ((apply_ptha then_conv vector_add_conv) else_conv
   14.16                arg_conv vector_add_conv then_conv apply_pthd)) ct)
   14.17        end
   14.18 -     | _ => reflexive ct))
   14.19 +     | _ => Thm.reflexive ct))
   14.20  
   14.21  fun vector_canon_conv ct = case term_of ct of
   14.22   Const(@{const_name plus},_)$_$_ =>
   14.23 @@ -237,7 +237,7 @@
   14.24  | Const(@{const_name vec},_)$n =>
   14.25    let val n = Thm.dest_arg ct
   14.26    in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero)
   14.27 -     then reflexive ct else apply_pth1 ct
   14.28 +     then Thm.reflexive ct else apply_pth1 ct
   14.29    end
   14.30  *)
   14.31  | _ => apply_pth1 ct
   14.32 @@ -342,7 +342,7 @@
   14.33    fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
   14.34    fun mk_norm t = Thm.capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
   14.35    fun mk_equals l r = Thm.capply (Thm.capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
   14.36 -  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
   14.37 +  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
   14.38    val replace_conv = try_conv (rewrs_conv asl)
   14.39    val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv))
   14.40    val ges' =
   14.41 @@ -352,10 +352,10 @@
   14.42    val nubs = map (conjunct2 o norm_mp) asl
   14.43    val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts')
   14.44    val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1))
   14.45 -  val th11 = hd (Variable.export ctxt' ctxt [fold implies_intr shs th1])
   14.46 +  val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
   14.47    val cps = map (swap o Thm.dest_equals) (cprems_of th11)
   14.48    val th12 = instantiate ([], cps) th11
   14.49 -  val th13 = fold Thm.elim_implies (map (reflexive o snd) cps) th12;
   14.50 +  val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
   14.51   in hd (Variable.export ctxt' ctxt [th13])
   14.52   end
   14.53  in val real_vector_ineq_prover = real_vector_ineq_prover
   14.54 @@ -390,7 +390,7 @@
   14.55    let
   14.56     val ctxt' = Variable.declare_term (term_of ct) ctxt
   14.57     val th = init_conv ctxt' ct
   14.58 -  in equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (symmetric th))
   14.59 +  in Thm.equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (Thm.symmetric th))
   14.60                  (pure ctxt' (Thm.rhs_of th))
   14.61   end
   14.62  
    15.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat May 15 21:41:32 2010 +0200
    15.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat May 15 21:50:05 2010 +0200
    15.3 @@ -602,7 +602,7 @@
    15.4          (fn _ => EVERY
    15.5             [indtac rep_induct [] 1,
    15.6              ALLGOALS (simp_tac (global_simpset_of thy4 addsimps
    15.7 -              (symmetric perm_fun_def :: abs_perm))),
    15.8 +              (Thm.symmetric perm_fun_def :: abs_perm))),
    15.9              ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])),
   15.10          length new_type_names));
   15.11  
   15.12 @@ -927,7 +927,7 @@
   15.13                 simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @
   15.14                   constr_defs @ perm_closed_thms)) 1,
   15.15                 TRY (simp_tac (HOL_basic_ss addsimps
   15.16 -                 (symmetric perm_fun_def :: abs_perm)) 1),
   15.17 +                 (Thm.symmetric perm_fun_def :: abs_perm)) 1),
   15.18                 TRY (simp_tac (HOL_basic_ss addsimps
   15.19                   (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
   15.20                      perm_closed_thms)) 1)])
   15.21 @@ -1077,7 +1077,7 @@
   15.22           (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   15.23           EVERY (map (fn (prem, r) => (EVERY
   15.24             [REPEAT (eresolve_tac Abs_inverse_thms' 1),
   15.25 -            simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
   15.26 +            simp_tac (HOL_basic_ss addsimps [Thm.symmetric r]) 1,
   15.27              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
   15.28                  (prems ~~ constr_defs))]);
   15.29  
   15.30 @@ -1641,7 +1641,7 @@
   15.31                            fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))]
   15.32                        supports_fresh) 1,
   15.33                      simp_tac (HOL_basic_ss addsimps
   15.34 -                      [supports_def, symmetric fresh_def, fresh_prod]) 1,
   15.35 +                      [supports_def, Thm.symmetric fresh_def, fresh_prod]) 1,
   15.36                      REPEAT_DETERM (resolve_tac [allI, impI] 1),
   15.37                      REPEAT_DETERM (etac conjE 1),
   15.38                      rtac unique 1,
   15.39 @@ -1655,7 +1655,7 @@
   15.40                      rtac rec_prem 1,
   15.41                      simp_tac (HOL_ss addsimps (fs_name ::
   15.42                        supp_prod :: finite_Un :: finite_prems)) 1,
   15.43 -                    simp_tac (HOL_ss addsimps (symmetric fresh_def ::
   15.44 +                    simp_tac (HOL_ss addsimps (Thm.symmetric fresh_def ::
   15.45                        fresh_prod :: fresh_prems)) 1]
   15.46                   end))
   15.47            end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ eqvt_ths)
   15.48 @@ -1746,7 +1746,7 @@
   15.49                 asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1])
   15.50                  (finite_thss ~~ finite_ctxt_ths) @
   15.51              maps (fn ((_, idxss), elim) => maps (fn idxs =>
   15.52 -              [full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff]) 1,
   15.53 +              [full_simp_tac (HOL_ss addsimps [Thm.symmetric fresh_def, supp_prod, Un_iff]) 1,
   15.54                 REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1),
   15.55                 rtac ex1I 1,
   15.56                 (resolve_tac rec_intrs THEN_ALL_NEW atac) 1,
    16.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sat May 15 21:41:32 2010 +0200
    16.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sat May 15 21:50:05 2010 +0200
    16.3 @@ -266,7 +266,7 @@
    16.4  (* intros, then applies eqvt_simp_tac                    *)
    16.5  fun supports_tac_i tactical ss i =
    16.6    let 
    16.7 -     val simps        = [supports_def,symmetric fresh_def,fresh_prod]
    16.8 +     val simps        = [supports_def, Thm.symmetric fresh_def, fresh_prod]
    16.9    in
   16.10        EVERY [tactical ("unfolding of supports   ", simp_tac (HOL_basic_ss addsimps simps) i),
   16.11               tactical ("stripping of foralls    ", REPEAT_DETERM (rtac allI i)),
   16.12 @@ -329,7 +329,7 @@
   16.13          val goal = List.nth(cprems_of st, i-1)
   16.14          val fin_supp = dynamic_thms st ("fin_supp")
   16.15          val fresh_atm = dynamic_thms st ("fresh_atm")
   16.16 -        val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
   16.17 +        val ss1 = ss addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
   16.18          val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
   16.19      in
   16.20        case Logic.strip_assums_concl (term_of goal) of
    17.1 --- a/src/HOL/Prolog/prolog.ML	Sat May 15 21:41:32 2010 +0200
    17.2 +++ b/src/HOL/Prolog/prolog.ML	Sat May 15 21:50:05 2010 +0200
    17.3 @@ -82,7 +82,7 @@
    17.4          val (prems, Const("Trueprop", _)$concl) = rep_goal
    17.5                                                  (#3(dest_state (st,i)));
    17.6  *)
    17.7 -        val subgoal = #3(dest_state (st,i));
    17.8 +        val subgoal = #3(Thm.dest_state (st,i));
    17.9          val prems = Logic.strip_assums_hyp subgoal;
   17.10          val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
   17.11          fun drot_tac k i = DETERM (rotate_tac k i);
    18.1 --- a/src/HOL/Statespace/state_fun.ML	Sat May 15 21:41:32 2010 +0200
    18.2 +++ b/src/HOL/Statespace/state_fun.ML	Sat May 15 21:50:05 2010 +0200
    18.3 @@ -245,7 +245,7 @@
    18.4                                        (fn _ => rtac meta_ext 1 THEN 
    18.5                                                 simp_tac ss1 1);
    18.6                       val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1));
    18.7 -                   in SOME (transitive eq1 eq2) end
    18.8 +                   in SOME (Thm.transitive eq1 eq2) end
    18.9               | _ => NONE)
   18.10           end
   18.11         | _ => NONE));
    19.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sat May 15 21:41:32 2010 +0200
    19.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sat May 15 21:50:05 2010 +0200
    19.3 @@ -483,8 +483,8 @@
    19.4             [(indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
    19.5              REPEAT (rtac TrueI 1),
    19.6              rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
    19.7 -              symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
    19.8 -            rewrite_goals_tac (map symmetric range_eqs),
    19.9 +              Thm.symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
   19.10 +            rewrite_goals_tac (map Thm.symmetric range_eqs),
   19.11              REPEAT (EVERY
   19.12                [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
   19.13                   maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
   19.14 @@ -621,7 +621,7 @@
   19.15           (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   19.16           EVERY (map (fn (prem, r) => (EVERY
   19.17             [REPEAT (eresolve_tac Abs_inverse_thms 1),
   19.18 -            simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
   19.19 +            simp_tac (HOL_basic_ss addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
   19.20              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
   19.21                  (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   19.22  
    20.1 --- a/src/HOL/Tools/Function/context_tree.ML	Sat May 15 21:41:32 2010 +0200
    20.2 +++ b/src/HOL/Tools/Function/context_tree.ML	Sat May 15 21:50:05 2010 +0200
    20.3 @@ -148,7 +148,7 @@
    20.4              val (r, dep, branches) = find_cong_rule ctx fvar h congs_deps t
    20.5              fun subtree (ctx', fixes, assumes, st) =
    20.6                ((fixes,
    20.7 -                map (assume o cterm_of (ProofContext.theory_of ctx)) assumes),
    20.8 +                map (Thm.assume o cterm_of (ProofContext.theory_of ctx)) assumes),
    20.9                 mk_tree' ctx' st)
   20.10            in
   20.11              Cong (r, dep, map subtree branches)
   20.12 @@ -165,7 +165,7 @@
   20.13      fun inst_term t =
   20.14        subst_bound(f, abstract_over (fvar, t))
   20.15  
   20.16 -    val inst_thm = forall_elim cf o forall_intr cfvar
   20.17 +    val inst_thm = Thm.forall_elim cf o Thm.forall_intr cfvar
   20.18  
   20.19      fun inst_tree_aux (Leaf t) = Leaf t
   20.20        | inst_tree_aux (Cong (crule, deps, branches)) =
   20.21 @@ -173,7 +173,7 @@
   20.22        | inst_tree_aux (RCall (t, str)) =
   20.23          RCall (inst_term t, inst_tree_aux str)
   20.24      and inst_branch ((fxs, assms), str) =
   20.25 -      ((fxs, map (assume o cterm_of thy o inst_term o prop_of) assms),
   20.26 +      ((fxs, map (Thm.assume o cterm_of thy o inst_term o prop_of) assms),
   20.27         inst_tree_aux str)
   20.28    in
   20.29      inst_tree_aux tr
   20.30 @@ -188,11 +188,11 @@
   20.31   #> fold_rev (Logic.all o Free) fixes
   20.32  
   20.33  fun export_thm thy (fixes, assumes) =
   20.34 - fold_rev (implies_intr o cprop_of) assumes
   20.35 - #> fold_rev (forall_intr o cterm_of thy o Free) fixes
   20.36 + fold_rev (Thm.implies_intr o cprop_of) assumes
   20.37 + #> fold_rev (Thm.forall_intr o cterm_of thy o Free) fixes
   20.38  
   20.39  fun import_thm thy (fixes, athms) =
   20.40 - fold (forall_elim o cterm_of thy o Free) fixes
   20.41 + fold (Thm.forall_elim o cterm_of thy o Free) fixes
   20.42   #> fold Thm.elim_implies athms
   20.43  
   20.44  
   20.45 @@ -241,7 +241,7 @@
   20.46  
   20.47  fun rewrite_by_tree thy h ih x tr =
   20.48    let
   20.49 -    fun rewrite_help _ _ x (Leaf t) = (reflexive (cterm_of thy t), x)
   20.50 +    fun rewrite_help _ _ x (Leaf t) = (Thm.reflexive (cterm_of thy t), x)
   20.51        | rewrite_help fix h_as x (RCall (_ $ arg, st)) =
   20.52          let
   20.53            val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *)
   20.54 @@ -250,11 +250,11 @@
   20.55              |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
   20.56                                                      (* (a, h a) : G   *)
   20.57            val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
   20.58 -          val eq = implies_elim (implies_elim inst_ih lRi) iha (* h a = f a *)
   20.59 +          val eq = Thm.implies_elim (Thm.implies_elim inst_ih lRi) iha (* h a = f a *)
   20.60  
   20.61 -          val h_a'_eq_h_a = combination (reflexive (cterm_of thy h)) inner
   20.62 +          val h_a'_eq_h_a = Thm.combination (Thm.reflexive (cterm_of thy h)) inner
   20.63            val h_a_eq_f_a = eq RS eq_reflection
   20.64 -          val result = transitive h_a'_eq_h_a h_a_eq_f_a
   20.65 +          val result = Thm.transitive h_a'_eq_h_a h_a_eq_f_a
   20.66          in
   20.67            (result, x')
   20.68          end
    21.1 --- a/src/HOL/Tools/Function/function_core.ML	Sat May 15 21:41:32 2010 +0200
    21.2 +++ b/src/HOL/Tools/Function/function_core.ML	Sat May 15 21:50:05 2010 +0200
    21.3 @@ -154,9 +154,9 @@
    21.4      val rhs = inst pre_rhs
    21.5  
    21.6      val cqs = map (cterm_of thy) qs
    21.7 -    val ags = map (assume o cterm_of thy) gs
    21.8 +    val ags = map (Thm.assume o cterm_of thy) gs
    21.9  
   21.10 -    val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
   21.11 +    val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
   21.12    in
   21.13      ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
   21.14        cqs = cqs, ags = ags, case_hyp = case_hyp }
   21.15 @@ -188,15 +188,15 @@
   21.16  
   21.17      (* Instantiate the GIntro thm with "f" and import into the clause context. *)
   21.18      val lGI = GIntro_thm
   21.19 -      |> forall_elim (cert f)
   21.20 -      |> fold forall_elim cqs
   21.21 +      |> Thm.forall_elim (cert f)
   21.22 +      |> fold Thm.forall_elim cqs
   21.23        |> fold Thm.elim_implies ags
   21.24  
   21.25      fun mk_call_info (rcfix, rcassm, rcarg) RI =
   21.26        let
   21.27          val llRI = RI
   21.28 -          |> fold forall_elim cqs
   21.29 -          |> fold (forall_elim o cert o Free) rcfix
   21.30 +          |> fold Thm.forall_elim cqs
   21.31 +          |> fold (Thm.forall_elim o cert o Free) rcfix
   21.32            |> fold Thm.elim_implies ags
   21.33            |> fold Thm.elim_implies rcassm
   21.34  
   21.35 @@ -242,20 +242,20 @@
   21.36        val compat = lookup_compat_thm j i cts
   21.37      in
   21.38        compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
   21.39 -      |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
   21.40 +      |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
   21.41        |> fold Thm.elim_implies agsj
   21.42        |> fold Thm.elim_implies agsi
   21.43 -      |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
   21.44 +      |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
   21.45      end
   21.46      else
   21.47      let
   21.48        val compat = lookup_compat_thm i j cts
   21.49      in
   21.50        compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
   21.51 -      |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
   21.52 +      |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
   21.53        |> fold Thm.elim_implies agsi
   21.54        |> fold Thm.elim_implies agsj
   21.55 -      |> Thm.elim_implies (assume lhsi_eq_lhsj)
   21.56 +      |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
   21.57        |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
   21.58      end
   21.59    end
   21.60 @@ -274,16 +274,16 @@
   21.61  
   21.62      val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
   21.63      val h_assums = map (fn RCInfo {h_assum, ...} =>
   21.64 -      assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
   21.65 +      Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
   21.66  
   21.67      val (eql, _) =
   21.68        Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
   21.69  
   21.70      val replace_lemma = (eql RS meta_eq_to_obj_eq)
   21.71 -      |> implies_intr (cprop_of case_hyp)
   21.72 -      |> fold_rev (implies_intr o cprop_of) h_assums
   21.73 -      |> fold_rev (implies_intr o cprop_of) ags
   21.74 -      |> fold_rev forall_intr cqs
   21.75 +      |> Thm.implies_intr (cprop_of case_hyp)
   21.76 +      |> fold_rev (Thm.implies_intr o cprop_of) h_assums
   21.77 +      |> fold_rev (Thm.implies_intr o cprop_of) ags
   21.78 +      |> fold_rev Thm.forall_intr cqs
   21.79        |> Thm.close_derivation
   21.80    in
   21.81      replace_lemma
   21.82 @@ -301,30 +301,30 @@
   21.83  
   21.84      val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
   21.85      val compat = get_compat_thm thy compat_store i j cctxi cctxj
   21.86 -    val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
   21.87 +    val Ghsj' = map (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
   21.88  
   21.89      val RLj_import = RLj
   21.90 -      |> fold forall_elim cqsj'
   21.91 +      |> fold Thm.forall_elim cqsj'
   21.92        |> fold Thm.elim_implies agsj'
   21.93        |> fold Thm.elim_implies Ghsj'
   21.94  
   21.95 -    val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
   21.96 -    val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
   21.97 +    val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
   21.98 +    val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
   21.99         (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
  21.100    in
  21.101      (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
  21.102 -    |> implies_elim RLj_import
  21.103 +    |> Thm.implies_elim RLj_import
  21.104        (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
  21.105      |> (fn it => trans OF [it, compat])
  21.106        (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
  21.107      |> (fn it => trans OF [y_eq_rhsj'h, it])
  21.108        (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
  21.109 -    |> fold_rev (implies_intr o cprop_of) Ghsj'
  21.110 -    |> fold_rev (implies_intr o cprop_of) agsj'
  21.111 +    |> fold_rev (Thm.implies_intr o cprop_of) Ghsj'
  21.112 +    |> fold_rev (Thm.implies_intr o cprop_of) agsj'
  21.113        (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
  21.114 -    |> implies_intr (cprop_of y_eq_rhsj'h)
  21.115 -    |> implies_intr (cprop_of lhsi_eq_lhsj')
  21.116 -    |> fold_rev forall_intr (cterm_of thy h :: cqsj')
  21.117 +    |> Thm.implies_intr (cprop_of y_eq_rhsj'h)
  21.118 +    |> Thm.implies_intr (cprop_of lhsi_eq_lhsj')
  21.119 +    |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')
  21.120    end
  21.121  
  21.122  
  21.123 @@ -338,13 +338,13 @@
  21.124      val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
  21.125  
  21.126      fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
  21.127 -      |> fold_rev (implies_intr o cprop_of) CCas
  21.128 -      |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
  21.129 +      |> fold_rev (Thm.implies_intr o cprop_of) CCas
  21.130 +      |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
  21.131  
  21.132      val existence = fold (curry op COMP o prep_RC) RCs lGI
  21.133  
  21.134      val P = cterm_of thy (mk_eq (y, rhsC))
  21.135 -    val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
  21.136 +    val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
  21.137  
  21.138      val unique_clauses =
  21.139        map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
  21.140 @@ -353,13 +353,13 @@
  21.141        Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
  21.142  
  21.143      val uniqueness = G_cases
  21.144 -      |> forall_elim (cterm_of thy lhs)
  21.145 -      |> forall_elim (cterm_of thy y)
  21.146 -      |> forall_elim P
  21.147 +      |> Thm.forall_elim (cterm_of thy lhs)
  21.148 +      |> Thm.forall_elim (cterm_of thy y)
  21.149 +      |> Thm.forall_elim P
  21.150        |> Thm.elim_implies G_lhs_y
  21.151        |> fold elim_implies_eta unique_clauses
  21.152 -      |> implies_intr (cprop_of G_lhs_y)
  21.153 -      |> forall_intr (cterm_of thy y)
  21.154 +      |> Thm.implies_intr (cprop_of G_lhs_y)
  21.155 +      |> Thm.forall_intr (cterm_of thy y)
  21.156  
  21.157      val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
  21.158  
  21.159 @@ -368,16 +368,16 @@
  21.160        |> curry (op COMP) existence
  21.161        |> curry (op COMP) uniqueness
  21.162        |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
  21.163 -      |> implies_intr (cprop_of case_hyp)
  21.164 -      |> fold_rev (implies_intr o cprop_of) ags
  21.165 -      |> fold_rev forall_intr cqs
  21.166 +      |> Thm.implies_intr (cprop_of case_hyp)
  21.167 +      |> fold_rev (Thm.implies_intr o cprop_of) ags
  21.168 +      |> fold_rev Thm.forall_intr cqs
  21.169  
  21.170      val function_value =
  21.171        existence
  21.172 -      |> implies_intr ihyp
  21.173 -      |> implies_intr (cprop_of case_hyp)
  21.174 -      |> forall_intr (cterm_of thy x)
  21.175 -      |> forall_elim (cterm_of thy lhs)
  21.176 +      |> Thm.implies_intr ihyp
  21.177 +      |> Thm.implies_intr (cprop_of case_hyp)
  21.178 +      |> Thm.forall_intr (cterm_of thy x)
  21.179 +      |> Thm.forall_elim (cterm_of thy lhs)
  21.180        |> curry (op RS) refl
  21.181    in
  21.182      (exactly_one, function_value)
  21.183 @@ -396,7 +396,7 @@
  21.184            Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
  21.185        |> cterm_of thy
  21.186  
  21.187 -    val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0
  21.188 +    val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
  21.189      val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
  21.190      val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
  21.191        |> instantiate' [] [NONE, SOME (cterm_of thy h)]
  21.192 @@ -412,17 +412,17 @@
  21.193      val graph_is_function = complete
  21.194        |> Thm.forall_elim_vars 0
  21.195        |> fold (curry op COMP) ex1s
  21.196 -      |> implies_intr (ihyp)
  21.197 -      |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
  21.198 -      |> forall_intr (cterm_of thy x)
  21.199 +      |> Thm.implies_intr (ihyp)
  21.200 +      |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
  21.201 +      |> Thm.forall_intr (cterm_of thy x)
  21.202        |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
  21.203 -      |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
  21.204 +      |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
  21.205  
  21.206      val goalstate =  Conjunction.intr graph_is_function complete
  21.207        |> Thm.close_derivation
  21.208        |> Goal.protect
  21.209 -      |> fold_rev (implies_intr o cprop_of) compat
  21.210 -      |> implies_intr (cprop_of complete)
  21.211 +      |> fold_rev (Thm.implies_intr o cprop_of) compat
  21.212 +      |> Thm.implies_intr (cprop_of complete)
  21.213    in
  21.214      (goalstate, values)
  21.215    end
  21.216 @@ -544,7 +544,7 @@
  21.217    let
  21.218      fun inst_term t = subst_bound(f, abstract_over (fvar, t))
  21.219    in
  21.220 -    (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
  21.221 +    (rcfix, map (Thm.assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
  21.222    end
  21.223  
  21.224  
  21.225 @@ -562,14 +562,14 @@
  21.226          val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
  21.227          val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
  21.228        in
  21.229 -        ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
  21.230 +        ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward))
  21.231          |> (fn it => it COMP graph_is_function)
  21.232 -        |> implies_intr z_smaller
  21.233 -        |> forall_intr (cterm_of thy z)
  21.234 +        |> Thm.implies_intr z_smaller
  21.235 +        |> Thm.forall_intr (cterm_of thy z)
  21.236          |> (fn it => it COMP valthm)
  21.237 -        |> implies_intr lhs_acc
  21.238 +        |> Thm.implies_intr lhs_acc
  21.239          |> asm_simplify (HOL_basic_ss addsimps [f_iff])
  21.240 -        |> fold_rev (implies_intr o cprop_of) ags
  21.241 +        |> fold_rev (Thm.implies_intr o cprop_of) ags
  21.242          |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  21.243        end
  21.244    in
  21.245 @@ -588,7 +588,7 @@
  21.246      val Globals {domT, x, z, a, P, D, ...} = globals
  21.247      val acc_R = mk_acc domT R
  21.248  
  21.249 -    val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
  21.250 +    val x_D = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
  21.251      val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
  21.252  
  21.253      val D_subset = cterm_of thy (Logic.all x
  21.254 @@ -606,7 +606,7 @@
  21.255          HOLogic.mk_Trueprop (P $ Bound 0)))
  21.256        |> cterm_of thy
  21.257  
  21.258 -    val aihyp = assume ihyp
  21.259 +    val aihyp = Thm.assume ihyp
  21.260  
  21.261      fun prove_case clause =
  21.262        let
  21.263 @@ -622,10 +622,10 @@
  21.264          end
  21.265  
  21.266          fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
  21.267 -          |> forall_elim (cterm_of thy rcarg)
  21.268 +          |> Thm.forall_elim (cterm_of thy rcarg)
  21.269            |> Thm.elim_implies llRI
  21.270 -          |> fold_rev (implies_intr o cprop_of) CCas
  21.271 -          |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
  21.272 +          |> fold_rev (Thm.implies_intr o cprop_of) CCas
  21.273 +          |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
  21.274  
  21.275          val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
  21.276  
  21.277 @@ -636,19 +636,19 @@
  21.278            |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  21.279            |> cterm_of thy
  21.280  
  21.281 -        val P_lhs = assume step
  21.282 -          |> fold forall_elim cqs
  21.283 +        val P_lhs = Thm.assume step
  21.284 +          |> fold Thm.forall_elim cqs
  21.285            |> Thm.elim_implies lhs_D
  21.286            |> fold Thm.elim_implies ags
  21.287            |> fold Thm.elim_implies P_recs
  21.288  
  21.289          val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
  21.290            |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
  21.291 -          |> symmetric (* P lhs == P x *)
  21.292 -          |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
  21.293 -          |> implies_intr (cprop_of case_hyp)
  21.294 -          |> fold_rev (implies_intr o cprop_of) ags
  21.295 -          |> fold_rev forall_intr cqs
  21.296 +          |> Thm.symmetric (* P lhs == P x *)
  21.297 +          |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *)
  21.298 +          |> Thm.implies_intr (cprop_of case_hyp)
  21.299 +          |> fold_rev (Thm.implies_intr o cprop_of) ags
  21.300 +          |> fold_rev Thm.forall_intr cqs
  21.301        in
  21.302          (res, step)
  21.303        end
  21.304 @@ -658,33 +658,33 @@
  21.305      val istep = complete_thm
  21.306        |> Thm.forall_elim_vars 0
  21.307        |> fold (curry op COMP) cases (*  P x  *)
  21.308 -      |> implies_intr ihyp
  21.309 -      |> implies_intr (cprop_of x_D)
  21.310 -      |> forall_intr (cterm_of thy x)
  21.311 +      |> Thm.implies_intr ihyp
  21.312 +      |> Thm.implies_intr (cprop_of x_D)
  21.313 +      |> Thm.forall_intr (cterm_of thy x)
  21.314  
  21.315      val subset_induct_rule =
  21.316        acc_subset_induct
  21.317 -      |> (curry op COMP) (assume D_subset)
  21.318 -      |> (curry op COMP) (assume D_dcl)
  21.319 -      |> (curry op COMP) (assume a_D)
  21.320 +      |> (curry op COMP) (Thm.assume D_subset)
  21.321 +      |> (curry op COMP) (Thm.assume D_dcl)
  21.322 +      |> (curry op COMP) (Thm.assume a_D)
  21.323        |> (curry op COMP) istep
  21.324 -      |> fold_rev implies_intr steps
  21.325 -      |> implies_intr a_D
  21.326 -      |> implies_intr D_dcl
  21.327 -      |> implies_intr D_subset
  21.328 +      |> fold_rev Thm.implies_intr steps
  21.329 +      |> Thm.implies_intr a_D
  21.330 +      |> Thm.implies_intr D_dcl
  21.331 +      |> Thm.implies_intr D_subset
  21.332  
  21.333      val simple_induct_rule =
  21.334        subset_induct_rule
  21.335 -      |> forall_intr (cterm_of thy D)
  21.336 -      |> forall_elim (cterm_of thy acc_R)
  21.337 +      |> Thm.forall_intr (cterm_of thy D)
  21.338 +      |> Thm.forall_elim (cterm_of thy acc_R)
  21.339        |> assume_tac 1 |> Seq.hd
  21.340        |> (curry op COMP) (acc_downward
  21.341          |> (instantiate' [SOME (ctyp_of thy domT)]
  21.342               (map (SOME o cterm_of thy) [R, x, z]))
  21.343 -        |> forall_intr (cterm_of thy z)
  21.344 -        |> forall_intr (cterm_of thy x))
  21.345 -      |> forall_intr (cterm_of thy a)
  21.346 -      |> forall_intr (cterm_of thy P)
  21.347 +        |> Thm.forall_intr (cterm_of thy z)
  21.348 +        |> Thm.forall_intr (cterm_of thy x))
  21.349 +      |> Thm.forall_intr (cterm_of thy a)
  21.350 +      |> Thm.forall_intr (cterm_of thy P)
  21.351    in
  21.352      simple_induct_rule
  21.353    end
  21.354 @@ -736,18 +736,19 @@
  21.355            |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  21.356            |> cterm_of thy
  21.357  
  21.358 -        val thm = assume hyp
  21.359 -          |> fold forall_elim cqs
  21.360 +        val thm = Thm.assume hyp
  21.361 +          |> fold Thm.forall_elim cqs
  21.362            |> fold Thm.elim_implies ags
  21.363            |> Function_Ctx_Tree.import_thm thy (fixes, assumes)
  21.364            |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
  21.365  
  21.366          val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg))
  21.367 -          |> cterm_of thy |> assume
  21.368 +          |> cterm_of thy |> Thm.assume
  21.369  
  21.370          val acc = thm COMP ih_case
  21.371          val z_acc_local = acc
  21.372 -          |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
  21.373 +          |> Conv.fconv_rule
  21.374 +              (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection)))))
  21.375  
  21.376          val ethm = z_acc_local
  21.377            |> Function_Ctx_Tree.export_thm thy (fixes,
  21.378 @@ -785,34 +786,34 @@
  21.379          HOLogic.mk_Trueprop (acc_R $ Bound 0)))
  21.380        |> cterm_of thy
  21.381  
  21.382 -    val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
  21.383 +    val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0
  21.384  
  21.385      val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
  21.386  
  21.387      val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], [])
  21.388    in
  21.389      R_cases
  21.390 -    |> forall_elim (cterm_of thy z)
  21.391 -    |> forall_elim (cterm_of thy x)
  21.392 -    |> forall_elim (cterm_of thy (acc_R $ z))
  21.393 -    |> curry op COMP (assume R_z_x)
  21.394 +    |> Thm.forall_elim (cterm_of thy z)
  21.395 +    |> Thm.forall_elim (cterm_of thy x)
  21.396 +    |> Thm.forall_elim (cterm_of thy (acc_R $ z))
  21.397 +    |> curry op COMP (Thm.assume R_z_x)
  21.398      |> fold_rev (curry op COMP) cases
  21.399 -    |> implies_intr R_z_x
  21.400 -    |> forall_intr (cterm_of thy z)
  21.401 +    |> Thm.implies_intr R_z_x
  21.402 +    |> Thm.forall_intr (cterm_of thy z)
  21.403      |> (fn it => it COMP accI)
  21.404 -    |> implies_intr ihyp
  21.405 -    |> forall_intr (cterm_of thy x)
  21.406 +    |> Thm.implies_intr ihyp
  21.407 +    |> Thm.forall_intr (cterm_of thy x)
  21.408      |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
  21.409 -    |> curry op RS (assume wfR')
  21.410 +    |> curry op RS (Thm.assume wfR')
  21.411      |> forall_intr_vars
  21.412      |> (fn it => it COMP allI)
  21.413 -    |> fold implies_intr hyps
  21.414 -    |> implies_intr wfR'
  21.415 -    |> forall_intr (cterm_of thy R')
  21.416 -    |> forall_elim (cterm_of thy (inrel_R))
  21.417 +    |> fold Thm.implies_intr hyps
  21.418 +    |> Thm.implies_intr wfR'
  21.419 +    |> Thm.forall_intr (cterm_of thy R')
  21.420 +    |> Thm.forall_elim (cterm_of thy (inrel_R))
  21.421      |> curry op RS wf_in_rel
  21.422      |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
  21.423 -    |> forall_intr (cterm_of thy Rrel)
  21.424 +    |> Thm.forall_intr (cterm_of thy Rrel)
  21.425    end
  21.426  
  21.427  
  21.428 @@ -919,11 +920,11 @@
  21.429          RCss GIntro_thms) RIntro_thmss
  21.430  
  21.431      val complete =
  21.432 -      mk_completeness globals clauses abstract_qglrs |> cert |> assume
  21.433 +      mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume
  21.434  
  21.435      val compat =
  21.436        mk_compat_proof_obligations domT ranT fvar f abstract_qglrs
  21.437 -      |> map (cert #> assume)
  21.438 +      |> map (cert #> Thm.assume)
  21.439  
  21.440      val compat_store = store_compat_thms n compat
  21.441  
    22.1 --- a/src/HOL/Tools/Function/function_lib.ML	Sat May 15 21:41:32 2010 +0200
    22.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Sat May 15 21:50:05 2010 +0200
    22.3 @@ -5,7 +5,7 @@
    22.4  Some fairly general functions that should probably go somewhere else...
    22.5  *)
    22.6  
    22.7 -structure Function_Lib =
    22.8 +structure Function_Lib =   (* FIXME proper signature *)
    22.9  struct
   22.10  
   22.11  fun map_option f NONE = NONE
   22.12 @@ -104,7 +104,7 @@
   22.13  
   22.14  fun forall_intr_rename (n, cv) thm =
   22.15    let
   22.16 -    val allthm = forall_intr cv thm
   22.17 +    val allthm = Thm.forall_intr cv thm
   22.18      val (_ $ abs) = prop_of allthm
   22.19    in
   22.20      Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm
    23.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Sat May 15 21:41:32 2010 +0200
    23.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Sat May 15 21:50:05 2010 +0200
    23.3 @@ -226,7 +226,7 @@
    23.4           HOLogic.mk_Trueprop (P_comp $ Bound 0)))
    23.5        |> cert
    23.6  
    23.7 -    val aihyp = assume ihyp
    23.8 +    val aihyp = Thm.assume ihyp
    23.9  
   23.10      (* Rule for case splitting along the sum types *)
   23.11      val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
   23.12 @@ -237,9 +237,9 @@
   23.13      fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
   23.14        let
   23.15          val fxs = map Free xs
   23.16 -        val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
   23.17 +        val branch_hyp = Thm.assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
   23.18  
   23.19 -        val C_hyps = map (cert #> assume) Cs
   23.20 +        val C_hyps = map (cert #> Thm.assume) Cs
   23.21  
   23.22          val (relevant_cases, ineqss') =
   23.23            (scases_idx ~~ ineqss)
   23.24 @@ -248,32 +248,33 @@
   23.25  
   23.26          fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
   23.27            let
   23.28 -            val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
   23.29 +            val case_hyps =
   23.30 +              map (Thm.assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
   23.31  
   23.32              val cqs = map (cert o Free) qs
   23.33 -            val ags = map (assume o cert) gs
   23.34 +            val ags = map (Thm.assume o cert) gs
   23.35  
   23.36              val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
   23.37              val sih = full_simplify replace_x_ss aihyp
   23.38  
   23.39              fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
   23.40                let
   23.41 -                val cGas = map (assume o cert) Gas
   23.42 +                val cGas = map (Thm.assume o cert) Gas
   23.43                  val cGvs = map (cert o Free) Gvs
   23.44 -                val import = fold forall_elim (cqs @ cGvs)
   23.45 +                val import = fold Thm.forall_elim (cqs @ cGvs)
   23.46                    #> fold Thm.elim_implies (ags @ cGas)
   23.47                  val ipres = pres
   23.48 -                  |> forall_elim (cert (list_comb (P_of idx, rcargs)))
   23.49 +                  |> Thm.forall_elim (cert (list_comb (P_of idx, rcargs)))
   23.50                    |> import
   23.51                in
   23.52                  sih
   23.53 -                |> forall_elim (cert (inject idx rcargs))
   23.54 +                |> Thm.forall_elim (cert (inject idx rcargs))
   23.55                  |> Thm.elim_implies (import ineq) (* Psum rcargs *)
   23.56                  |> Conv.fconv_rule sum_prod_conv
   23.57                  |> Conv.fconv_rule ind_rulify
   23.58                  |> (fn th => th COMP ipres) (* P rs *)
   23.59 -                |> fold_rev (implies_intr o cprop_of) cGas
   23.60 -                |> fold_rev forall_intr cGvs
   23.61 +                |> fold_rev (Thm.implies_intr o cprop_of) cGas
   23.62 +                |> fold_rev Thm.forall_intr cGvs
   23.63                end
   23.64  
   23.65              val P_recs = map2 mk_Prec rs ineq_press   (*  [P rec1, P rec2, ... ]  *)
   23.66 @@ -288,13 +289,13 @@
   23.67                foldl1 (uncurry Conv.combination_conv)
   23.68                  (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps)
   23.69  
   23.70 -            val res = assume step
   23.71 -              |> fold forall_elim cqs
   23.72 +            val res = Thm.assume step
   23.73 +              |> fold Thm.forall_elim cqs
   23.74                |> fold Thm.elim_implies ags
   23.75                |> fold Thm.elim_implies P_recs (* P lhs *)
   23.76                |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *)
   23.77 -              |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps)
   23.78 -              |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
   23.79 +              |> fold_rev (Thm.implies_intr o cprop_of) (ags @ case_hyps)
   23.80 +              |> fold_rev Thm.forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
   23.81            in
   23.82              (res, (cidx, step))
   23.83            end
   23.84 @@ -302,12 +303,12 @@
   23.85          val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
   23.86  
   23.87          val bstep = complete_thm
   23.88 -          |> forall_elim (cert (list_comb (P, fxs)))
   23.89 -          |> fold (forall_elim o cert) (fxs @ map Free ws)
   23.90 +          |> Thm.forall_elim (cert (list_comb (P, fxs)))
   23.91 +          |> fold (Thm.forall_elim o cert) (fxs @ map Free ws)
   23.92            |> fold Thm.elim_implies C_hyps
   23.93            |> fold Thm.elim_implies cases (* P xs *)
   23.94 -          |> fold_rev (implies_intr o cprop_of) C_hyps
   23.95 -          |> fold_rev (forall_intr o cert o Free) ws
   23.96 +          |> fold_rev (Thm.implies_intr o cprop_of) C_hyps
   23.97 +          |> fold_rev (Thm.forall_intr o cert o Free) ws
   23.98  
   23.99          val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
  23.100            |> Goal.init
  23.101 @@ -316,8 +317,8 @@
  23.102            |> Seq.hd
  23.103            |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
  23.104            |> Goal.finish ctxt
  23.105 -          |> implies_intr (cprop_of branch_hyp)
  23.106 -          |> fold_rev (forall_intr o cert) fxs
  23.107 +          |> Thm.implies_intr (cprop_of branch_hyp)
  23.108 +          |> fold_rev (Thm.forall_intr o cert) fxs
  23.109        in
  23.110          (Pxs, steps)
  23.111        end
  23.112 @@ -328,8 +329,8 @@
  23.113  
  23.114      val istep = sum_split_rule
  23.115        |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
  23.116 -      |> implies_intr ihyp
  23.117 -      |> forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
  23.118 +      |> Thm.implies_intr ihyp
  23.119 +      |> Thm.forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
  23.120  
  23.121      val induct_rule =
  23.122        @{thm "wf_induct_rule"}
  23.123 @@ -353,10 +354,10 @@
  23.124      val cert = cterm_of (ProofContext.theory_of ctxt)
  23.125  
  23.126      val ineqss = mk_ineqs R scheme
  23.127 -      |> map (map (pairself (assume o cert)))
  23.128 +      |> map (map (pairself (Thm.assume o cert)))
  23.129      val complete =
  23.130 -      map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
  23.131 -    val wf_thm = mk_wf R scheme |> cert |> assume
  23.132 +      map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches)
  23.133 +    val wf_thm = mk_wf R scheme |> cert |> Thm.assume
  23.134  
  23.135      val (descent, pres) = split_list (flat ineqss)
  23.136      val newgoals = complete @ pres @ wf_thm :: descent
  23.137 @@ -377,7 +378,7 @@
  23.138        end
  23.139  
  23.140      val res = Conjunction.intr_balanced (map_index project branches)
  23.141 -      |> fold_rev implies_intr (map cprop_of newgoals @ steps)
  23.142 +      |> fold_rev Thm.implies_intr (map cprop_of newgoals @ steps)
  23.143        |> Drule.generalize ([], [Rn])
  23.144  
  23.145      val nbranches = length branches
    24.1 --- a/src/HOL/Tools/Function/mutual.ML	Sat May 15 21:41:32 2010 +0200
    24.2 +++ b/src/HOL/Tools/Function/mutual.ML	Sat May 15 21:50:05 2010 +0200
    24.3 @@ -164,12 +164,12 @@
    24.4      val rhs = inst pre_rhs
    24.5  
    24.6      val cqs = map (cterm_of thy) qs
    24.7 -    val ags = map (assume o cterm_of thy) gs
    24.8 +    val ags = map (Thm.assume o cterm_of thy) gs
    24.9  
   24.10 -    val import = fold forall_elim cqs
   24.11 +    val import = fold Thm.forall_elim cqs
   24.12        #> fold Thm.elim_implies ags
   24.13  
   24.14 -    val export = fold_rev (implies_intr o cprop_of) ags
   24.15 +    val export = fold_rev (Thm.implies_intr o cprop_of) ags
   24.16        #> fold_rev forall_intr_rename (oqnames ~~ cqs)
   24.17    in
   24.18      F ctxt (f, qs, gs, args, rhs) import export
   24.19 @@ -184,7 +184,7 @@
   24.20      val (simp, restore_cond) =
   24.21        case cprems_of psimp of
   24.22          [] => (psimp, I)
   24.23 -      | [cond] => (implies_elim psimp (assume cond), implies_intr cond)
   24.24 +      | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
   24.25        | _ => sys_error "Too many conditions"
   24.26  
   24.27    in
   24.28 @@ -202,9 +202,9 @@
   24.29      val thy = ProofContext.theory_of ctxt
   24.30      val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
   24.31    in
   24.32 -    fold (fn x => fn thm => combination thm (reflexive x)) xs thm
   24.33 +    fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm
   24.34      |> Conv.fconv_rule (Thm.beta_conversion true)
   24.35 -    |> fold_rev forall_intr xs
   24.36 +    |> fold_rev Thm.forall_intr xs
   24.37      |> Thm.forall_elim_vars 0
   24.38    end
   24.39  
   24.40 @@ -228,7 +228,7 @@
   24.41      val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps
   24.42  
   24.43      val induct_inst =
   24.44 -      forall_elim (cert case_exp) induct
   24.45 +      Thm.forall_elim (cert case_exp) induct
   24.46        |> full_simplify SumTree.sumcase_split_ss
   24.47        |> full_simplify (HOL_basic_ss addsimps all_f_defs)
   24.48  
   24.49 @@ -238,9 +238,9 @@
   24.50          val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
   24.51        in
   24.52          (rule
   24.53 -         |> forall_elim (cert inj)
   24.54 +         |> Thm.forall_elim (cert inj)
   24.55           |> full_simplify SumTree.sumcase_split_ss
   24.56 -         |> fold_rev (forall_intr o cert) (afs @ newPs),
   24.57 +         |> fold_rev (Thm.forall_intr o cert) (afs @ newPs),
   24.58           k + length cargTs)
   24.59        end
   24.60    in
   24.61 @@ -255,7 +255,7 @@
   24.62  
   24.63      val (all_f_defs, fs) =
   24.64        map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
   24.65 -        (mk_applied_form lthy cargTs (symmetric f_def), f))
   24.66 +        (mk_applied_form lthy cargTs (Thm.symmetric f_def), f))
   24.67        parts
   24.68        |> split_list
   24.69  
    25.1 --- a/src/HOL/Tools/Function/pat_completeness.ML	Sat May 15 21:41:32 2010 +0200
    25.2 +++ b/src/HOL/Tools/Function/pat_completeness.ML	Sat May 15 21:50:05 2010 +0200
    25.3 @@ -24,7 +24,7 @@
    25.4  fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
    25.5  fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
    25.6  
    25.7 -fun inst_free var inst = forall_elim inst o forall_intr var
    25.8 +fun inst_free var inst = Thm.forall_elim inst o Thm.forall_intr var
    25.9  
   25.10  fun inst_case_thm thy x P thm =
   25.11    let val [Pv, xv] = Term.add_vars (prop_of thm) []
   25.12 @@ -69,10 +69,10 @@
   25.13    let
   25.14      val (_, subps) = strip_comb pat
   25.15      val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
   25.16 -    val c_eq_pat = simplify (HOL_basic_ss addsimps (map assume eqs)) c_assum
   25.17 +    val c_eq_pat = simplify (HOL_basic_ss addsimps (map Thm.assume eqs)) c_assum
   25.18    in
   25.19      (subps @ pats,
   25.20 -     fold_rev implies_intr eqs (implies_elim thm c_eq_pat))
   25.21 +     fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat))
   25.22    end
   25.23  
   25.24  
   25.25 @@ -82,12 +82,12 @@
   25.26    let
   25.27      val (avars, pvars, newidx) = invent_vars cons idx
   25.28      val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
   25.29 -    val c_assum = assume c_hyp
   25.30 +    val c_assum = Thm.assume c_hyp
   25.31      val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats)
   25.32    in
   25.33      o_alg thy P newidx (avars @ vs) newpats
   25.34 -    |> implies_intr c_hyp
   25.35 -    |> fold_rev (forall_intr o cterm_of thy) avars
   25.36 +    |> Thm.implies_intr c_hyp
   25.37 +    |> fold_rev (Thm.forall_intr o cterm_of thy) avars
   25.38    end
   25.39    | constr_case _ _ _ _ _ _ = raise Match
   25.40  and o_alg thy P idx [] (([], Pthm) :: _)  = Pthm
   25.41 @@ -119,11 +119,11 @@
   25.42        |> cterm_of thy
   25.43  
   25.44      val hyps = map2 mk_assum qss patss
   25.45 -    fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp)
   25.46 +    fun inst_hyps hyp qs = fold (Thm.forall_elim o cterm_of thy) qs (Thm.assume hyp)
   25.47      val assums = map2 inst_hyps hyps qss
   25.48      in
   25.49        o_alg thy P 2 xs (patss ~~ assums)
   25.50 -      |> fold_rev implies_intr hyps
   25.51 +      |> fold_rev Thm.implies_intr hyps
   25.52      end
   25.53  
   25.54  fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) =>
   25.55 @@ -147,7 +147,7 @@
   25.56  
   25.57      val patss = map (map snd) x_pats
   25.58      val complete_thm = prove_completeness thy xs thesis qss patss
   25.59 -      |> fold_rev (forall_intr o cterm_of thy) vs
   25.60 +      |> fold_rev (Thm.forall_intr o cterm_of thy) vs
   25.61      in
   25.62        PRIMITIVE (fn st => Drule.compose_single(complete_thm, i, st))
   25.63    end
    26.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat May 15 21:41:32 2010 +0200
    26.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat May 15 21:50:05 2010 +0200
    26.3 @@ -331,7 +331,7 @@
    26.4  | t => if is_intrel t
    26.5        then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop))
    26.6         RS eq_reflection
    26.7 -      else reflexive ct;
    26.8 +      else Thm.reflexive ct;
    26.9  
   26.10  val dvdc = @{cterm "op dvd :: int => _"};
   26.11  
   26.12 @@ -369,7 +369,7 @@
   26.13        (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}
   26.14             (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
   26.15             @{cterm "0::int"})))
   26.16 -   in equal_elim (Thm.symmetric th) TrueI end;
   26.17 +   in Thm.equal_elim (Thm.symmetric th) TrueI end;
   26.18    val notz =
   26.19      let val tab = fold Inttab.update
   26.20            (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
   26.21 @@ -412,11 +412,11 @@
   26.22    val ltx = Thm.capply (Thm.capply cmulC clt) cx
   26.23    val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth)
   26.24    val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex
   26.25 -  val thf = transitive th
   26.26 -      (transitive (symmetric (beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
   26.27 +  val thf = Thm.transitive th
   26.28 +      (Thm.transitive (Thm.symmetric (Thm.beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
   26.29    val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true
   26.30 -                  ||> beta_conversion true |>> Thm.symmetric
   26.31 - in transitive (transitive lth thf) rth end;
   26.32 +                  ||> Thm.beta_conversion true |>> Thm.symmetric
   26.33 + in Thm.transitive (Thm.transitive lth thf) rth end;
   26.34  
   26.35  
   26.36  val emptyIS = @{cterm "{}::int set"};
   26.37 @@ -459,7 +459,7 @@
   26.38       Simplifier.rewrite lin_ss
   26.39        (Thm.capply @{cterm Trueprop}
   26.40             (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
   26.41 -   in equal_elim (Thm.symmetric th) TrueI end;
   26.42 +   in Thm.equal_elim (Thm.symmetric th) TrueI end;
   26.43   val dvd =
   26.44     let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
   26.45       fn ct => the (Inttab.lookup tab (term_of ct |> dest_number))
   26.46 @@ -471,7 +471,7 @@
   26.47     let val th = Simplifier.rewrite lin_ss
   26.48        (Thm.capply @{cterm Trueprop}
   26.49             (Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
   26.50 -   in equal_elim (Thm.symmetric th) TrueI end;
   26.51 +   in Thm.equal_elim (Thm.symmetric th) TrueI end;
   26.52      (* A and B set *)
   26.53     local
   26.54       val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
   26.55 @@ -483,7 +483,7 @@
   26.56        | Const(@{const_name insert}, _) $ y $ _ =>
   26.57           let val (cy,S') = Thm.dest_binop S
   26.58           in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
   26.59 -         else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
   26.60 +         else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
   26.61                             (provein x S')
   26.62           end
   26.63     end
   26.64 @@ -494,14 +494,14 @@
   26.65     if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)
   26.66     then
   26.67      (bl,b0,decomp_minf,
   26.68 -     fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
   26.69 +     fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
   26.70                       [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@
   26.71                     (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]))
   26.72                          [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj,
   26.73                           bsetdisj,infDconj, infDdisj]),
   26.74                         cpmi)
   26.75       else (al,a0,decomp_pinf,fn A =>
   26.76 -          (map (fn th => implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
   26.77 +          (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
   26.78                     [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@
   26.79                     (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]))
   26.80                     [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,
   26.81 @@ -776,7 +776,7 @@
   26.82     fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
   26.83     val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
   26.84     val p' = fold_rev gen ts p
   26.85 - in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
   26.86 + in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
   26.87  
   26.88  local
   26.89  val ss1 = comp_ss
   26.90 @@ -792,7 +792,7 @@
   26.91              @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
   26.92    addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
   26.93  val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms}
   26.94 -  @ map (symmetric o mk_meta_eq) 
   26.95 +  @ map (Thm.symmetric o mk_meta_eq) 
   26.96      [@{thm "dvd_eq_mod_eq_0"},
   26.97       @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
   26.98       @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
   26.99 @@ -823,7 +823,7 @@
  26.100         then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
  26.101         else Conv.arg_conv (conv ctxt) p
  26.102      val p' = Thm.rhs_of cpth
  26.103 -    val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
  26.104 +    val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
  26.105     in rtac th i end
  26.106     handle COOPER _ => no_tac);
  26.107  
    27.1 --- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Sat May 15 21:41:32 2010 +0200
    27.2 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Sat May 15 21:50:05 2010 +0200
    27.3 @@ -69,7 +69,7 @@
    27.4        val th0 = if mi then
    27.5             instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
    27.6          else instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
    27.7 -     in implies_elim (implies_elim th0 th') th'' end
    27.8 +     in Thm.implies_elim (Thm.implies_elim th0 th') th'' end
    27.9    in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
   27.10        fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
   27.11    end
   27.12 @@ -88,7 +88,7 @@
   27.13     val enth = Drule.arg_cong_rule ce nthx
   27.14     val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
   27.15     fun ins x th =
   27.16 -      implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
   27.17 +      Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
   27.18                                         (Thm.cprop_of th), SOME x] th1) th
   27.19     val fU = fold ins u th0
   27.20     val cU = funpow 2 Thm.dest_arg (Thm.cprop_of fU)
   27.21 @@ -102,7 +102,7 @@
   27.22        | Const(@{const_name insert}, _) $ y $_ =>
   27.23           let val (cy,S') = Thm.dest_binop S
   27.24           in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
   27.25 -         else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
   27.26 +         else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
   27.27                             (provein x S')
   27.28           end
   27.29     end
   27.30 @@ -152,7 +152,7 @@
   27.31                            | Eq => [minf_eq, pinf_eq, nmi_eq, npi_eq, ld_eq]
   27.32                            | NEq => [minf_neq, pinf_neq, nmi_neq, npi_neq, ld_neq])
   27.33                      val tU = U t
   27.34 -                    fun Ufw th = implies_elim th tU
   27.35 +                    fun Ufw th = Thm.implies_elim th tU
   27.36                   in [mi_th, pi_th, Ufw nmi_th, Ufw npi_th, Ufw ld_th]
   27.37                   end
   27.38           in ([], K (mi_th, pi_th, nmi_th, npi_th, ld_th)) end)
   27.39 @@ -164,7 +164,7 @@
   27.40                    [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
   27.41      val bex_conv =
   27.42        Simplifier.rewrite (HOL_basic_ss addsimps simp_thms@(@{thms "bex_simps" (1-5)}))
   27.43 -    val result_th = fconv_rule (arg_conv bex_conv) (transitive enth qe_th)
   27.44 +    val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th)
   27.45     in result_th
   27.46     end
   27.47  
    28.1 --- a/src/HOL/Tools/Qelim/langford.ML	Sat May 15 21:41:32 2010 +0200
    28.2 +++ b/src/HOL/Tools/Qelim/langford.ML	Sat May 15 21:50:05 2010 +0200
    28.3 @@ -22,7 +22,7 @@
    28.4  fun prove_finite cT u = 
    28.5  let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
    28.6      fun ins x th =
    28.7 -     implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
    28.8 +     Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
    28.9                                       (Thm.cprop_of th), SOME x] th1) th
   28.10  in fold ins u th0 end;
   28.11  
   28.12 @@ -51,17 +51,17 @@
   28.13        (Const (@{const_name Orderings.bot}, _),_) =>  
   28.14          let
   28.15            val (neU,fU) = proveneF U 
   28.16 -        in simp_rule (transitive ths (dlo_qeth_nolb OF [neU, fU])) end
   28.17 +        in simp_rule (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
   28.18      | (_,Const (@{const_name Orderings.bot}, _)) =>  
   28.19          let
   28.20            val (neL,fL) = proveneF L
   28.21 -        in simp_rule (transitive ths (dlo_qeth_noub OF [neL, fL])) end
   28.22 +        in simp_rule (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
   28.23  
   28.24      | (_,_) =>  
   28.25        let 
   28.26         val (neL,fL) = proveneF L
   28.27         val (neU,fU) = proveneF U
   28.28 -      in simp_rule (transitive ths (dlo_qeth OF [neL, neU, fL, fU])) 
   28.29 +      in simp_rule (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU])) 
   28.30        end
   28.31     in qe end 
   28.32   | _ => error "dlo_qe : Not an existential formula";
   28.33 @@ -101,8 +101,8 @@
   28.34  fun conj_aci_rule eq = 
   28.35   let 
   28.36    val (l,r) = Thm.dest_equals eq
   28.37 -  fun tabl c = the (Termtab.lookup (mk_conj_tab (assume l)) (term_of c))
   28.38 -  fun tabr c = the (Termtab.lookup (mk_conj_tab (assume r)) (term_of c))
   28.39 +  fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c))
   28.40 +  fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c))
   28.41    val ll = Thm.dest_arg l
   28.42    val rr = Thm.dest_arg r
   28.43    
   28.44 @@ -111,7 +111,7 @@
   28.45    val thr  = prove_conj tabr (conjuncts ll) 
   28.46                  |> Drule.implies_intr_hyps
   28.47    val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
   28.48 - in implies_elim (implies_elim eqI thl) thr |> mk_meta_eq end;
   28.49 + in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
   28.50  
   28.51  fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
   28.52  
   28.53 @@ -136,7 +136,7 @@
   28.54                        | _ =>
   28.55              conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp 
   28.56                   (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx))))
   28.57 -           |> abstract_rule xn x |> Drule.arg_cong_rule e 
   28.58 +           |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
   28.59             |> Conv.fconv_rule (Conv.arg_conv 
   28.60                     (Simplifier.rewrite 
   28.61                        (HOL_basic_ss addsimps (simp_thms @ ex_simps))))
   28.62 @@ -144,7 +144,7 @@
   28.63            end
   28.64      | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp 
   28.65                   (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs))))
   28.66 -           |> abstract_rule xn x |> Drule.arg_cong_rule e 
   28.67 +           |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
   28.68             |> Conv.fconv_rule (Conv.arg_conv 
   28.69                     (Simplifier.rewrite 
   28.70                  (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) 
   28.71 @@ -167,7 +167,7 @@
   28.72                  @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib])
   28.73   in fn p => 
   28.74     Qelim.gen_qelim_conv pcv pcv dnfex_conv cons 
   28.75 -                  (Thm.add_cterm_frees p [])  (K reflexive) (K reflexive)
   28.76 +                  (Thm.add_cterm_frees p [])  (K Thm.reflexive) (K Thm.reflexive)
   28.77                    (K (basic_dloqe () gst qe_bnds qe_nolb qe_noub gs)) p
   28.78   end;
   28.79  
   28.80 @@ -212,7 +212,7 @@
   28.81     fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
   28.82     val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
   28.83     val p' = fold_rev gen ts p
   28.84 - in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
   28.85 + in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
   28.86  
   28.87  
   28.88  fun cfrees ats ct =
    29.1 --- a/src/HOL/Tools/Qelim/qelim.ML	Sat May 15 21:41:32 2010 +0200
    29.2 +++ b/src/HOL/Tools/Qelim/qelim.ML	Sat May 15 21:50:05 2010 +0200
    29.3 @@ -47,7 +47,7 @@
    29.4       val p = Thm.dest_arg p
    29.5       val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
    29.6       val th = instantiate' [SOME T] [SOME p] all_not_ex
    29.7 -    in transitive th (conv env (Thm.rhs_of th))
    29.8 +    in Thm.transitive th (conv env (Thm.rhs_of th))
    29.9      end
   29.10    | _ => atcv env p
   29.11   in precv then_conv (conv env) then_conv postcv end
    30.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat May 15 21:41:32 2010 +0200
    30.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat May 15 21:50:05 2010 +0200
    30.3 @@ -517,7 +517,7 @@
    30.4  *)
    30.5  fun clean_tac lthy =
    30.6  let
    30.7 -  val defs = map (symmetric o #def) (qconsts_dest lthy)
    30.8 +  val defs = map (Thm.symmetric o #def) (qconsts_dest lthy)
    30.9    val prs = prs_rules_get lthy
   30.10    val ids = id_simps_get lthy
   30.11    val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
    31.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Sat May 15 21:41:32 2010 +0200
    31.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Sat May 15 21:50:05 2010 +0200
    31.3 @@ -35,7 +35,7 @@
    31.4  (* Useful Theorems                                                           *)
    31.5  (* ------------------------------------------------------------------------- *)
    31.6  val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
    31.7 -val REFL_THM = incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
    31.8 +val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
    31.9  val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
   31.10  val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
   31.11  
   31.12 @@ -364,7 +364,7 @@
   31.13    in  cterm_instantiate substs th  end;
   31.14  
   31.15  (* INFERENCE RULE: AXIOM *)
   31.16 -fun axiom_inf thpairs th = incr_indexes 1 (lookth thpairs th);
   31.17 +fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
   31.18      (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
   31.19  
   31.20  (* INFERENCE RULE: ASSUME *)
   31.21 @@ -527,7 +527,7 @@
   31.22        val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   31.23        val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   31.24        val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   31.25 -      val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   31.26 +      val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   31.27        val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   31.28        val eq_terms = map (pairself (cterm_of thy))
   31.29          (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
    32.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat May 15 21:41:32 2010 +0200
    32.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat May 15 21:50:05 2010 +0200
    32.3 @@ -209,7 +209,7 @@
    32.4                     Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
    32.5                   end
    32.6              else if loose_bvar1 (rand,0) then (*B or eta*)
    32.7 -               if rand = Bound 0 then eta_conversion ct
    32.8 +               if rand = Bound 0 then Thm.eta_conversion ct
    32.9                 else (*B*)
   32.10                   let val crand = cterm_of thy (Abs(x,xT,rand))
   32.11                       val crator = cterm_of thy rator
   32.12 @@ -225,7 +225,7 @@
   32.13  (*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
   32.14    prefix for the constants.*)
   32.15  fun combinators_aux ct =
   32.16 -  if lambda_free (term_of ct) then reflexive ct
   32.17 +  if lambda_free (term_of ct) then Thm.reflexive ct
   32.18    else
   32.19    case term_of ct of
   32.20        Abs _ =>
   32.21 @@ -234,17 +234,17 @@
   32.22              val u_th = combinators_aux cta
   32.23              val cu = Thm.rhs_of u_th
   32.24              val comb_eq = abstract (Thm.cabs cv cu)
   32.25 -        in transitive (abstract_rule v cv u_th) comb_eq end
   32.26 +        in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
   32.27      | _ $ _ =>
   32.28          let val (ct1, ct2) = Thm.dest_comb ct
   32.29 -        in  combination (combinators_aux ct1) (combinators_aux ct2)  end;
   32.30 +        in  Thm.combination (combinators_aux ct1) (combinators_aux ct2)  end;
   32.31  
   32.32  fun combinators th =
   32.33    if lambda_free (prop_of th) then th
   32.34    else
   32.35      let val th = Drule.eta_contraction_rule th
   32.36          val eqth = combinators_aux (cprop_of th)
   32.37 -    in  equal_elim eqth th   end
   32.38 +    in  Thm.equal_elim eqth th   end
   32.39      handle THM (msg,_,_) =>
   32.40        (warning (cat_lines
   32.41          ["Error in the combinator translation of " ^ Display.string_of_thm_without_context th,
   32.42 @@ -298,7 +298,7 @@
   32.43  
   32.44  (*Generate Skolem functions for a theorem supplied in nnf*)
   32.45  fun assume_skolem_of_def s th =
   32.46 -  map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
   32.47 +  map (skolem_of_def o Thm.assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
   32.48  
   32.49  
   32.50  (*** Blacklisting (FIXME: duplicated in "Sledgehammer_Fact_Filter"?) ***)
    33.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Sat May 15 21:41:32 2010 +0200
    33.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Sat May 15 21:50:05 2010 +0200
    33.3 @@ -79,8 +79,8 @@
    33.4  (* beta-eta contract the theorem *)
    33.5  fun beta_eta_contract thm =
    33.6      let
    33.7 -      val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
    33.8 -      val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
    33.9 +      val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
   33.10 +      val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
   33.11      in thm3 end;
   33.12  
   33.13  (* make a casethm from an induction thm *)
    34.1 --- a/src/HOL/Tools/TFL/rules.ML	Sat May 15 21:41:32 2010 +0200
    34.2 +++ b/src/HOL/Tools/TFL/rules.ML	Sat May 15 21:50:05 2010 +0200
    34.3 @@ -172,7 +172,7 @@
    34.4        val [P,Q] = OldTerm.term_vars prop
    34.5        val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
    34.6  in
    34.7 -fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
    34.8 +fun DISJ1 thm tm = thm RS (Thm.forall_elim (D.drop_prop tm) disj1)
    34.9    handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
   34.10  end;
   34.11  
   34.12 @@ -181,7 +181,7 @@
   34.13        val [P,Q] = OldTerm.term_vars prop
   34.14        val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
   34.15  in
   34.16 -fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
   34.17 +fun DISJ2 tm thm = thm RS (Thm.forall_elim (D.drop_prop tm) disj2)
   34.18    handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
   34.19  end;
   34.20  
   34.21 @@ -276,11 +276,11 @@
   34.22        val prop = Thm.prop_of spec
   34.23        val x = hd (tl (OldTerm.term_vars prop))
   34.24        val cTV = ctyp_of thy (type_of x)
   34.25 -      val gspec = forall_intr (cterm_of thy x) spec
   34.26 +      val gspec = Thm.forall_intr (cterm_of thy x) spec
   34.27  in
   34.28  fun SPEC tm thm =
   34.29     let val gspec' = instantiate ([(cTV, Thm.ctyp_of_term tm)], []) gspec
   34.30 -   in thm RS (forall_elim tm gspec') end
   34.31 +   in thm RS (Thm.forall_elim tm gspec') end
   34.32  end;
   34.33  
   34.34  fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm;
   34.35 @@ -302,7 +302,7 @@
   34.36           ctm_theta s (Vartab.dest tm_theta))
   34.37  in
   34.38  fun GEN v th =
   34.39 -   let val gth = forall_intr v th
   34.40 +   let val gth = Thm.forall_intr v th
   34.41         val thy = Thm.theory_of_thm gth
   34.42         val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth
   34.43         val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
   34.44 @@ -533,9 +533,9 @@
   34.45   *---------------------------------------------------------------------------*)
   34.46  
   34.47  fun list_beta_conv tm =
   34.48 -  let fun rbeta th = Thm.transitive th (beta_conversion false (#2(D.dest_eq(cconcl th))))
   34.49 +  let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(D.dest_eq(cconcl th))))
   34.50        fun iter [] = Thm.reflexive tm
   34.51 -        | iter (v::rst) = rbeta (combination(iter rst) (Thm.reflexive v))
   34.52 +        | iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v))
   34.53    in iter  end;
   34.54  
   34.55  
   34.56 @@ -619,7 +619,7 @@
   34.57  fun VSTRUCT_ELIM tych a vstr th =
   34.58    let val L = S.free_vars_lr vstr
   34.59        val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
   34.60 -      val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th)
   34.61 +      val thm1 = Thm.implies_intr bind1 (SUBS [SYM(Thm.assume bind1)] th)
   34.62        val thm2 = forall_intr_list (map tych L) thm1
   34.63        val thm3 = forall_elim_list (XFILL tych a vstr) thm2
   34.64    in refl RS
   34.65 @@ -630,7 +630,7 @@
   34.66    let val a1 = tych a
   34.67        val vstr1 = tych vstr
   34.68    in
   34.69 -  forall_intr a1
   34.70 +  Thm.forall_intr a1
   34.71       (if (is_Free vstr)
   34.72        then cterm_instantiate [(vstr1,a1)] th
   34.73        else VSTRUCT_ELIM tych a vstr th)
   34.74 @@ -803,7 +803,7 @@
   34.75      val names = OldTerm.add_term_names (term_of ctm, [])
   34.76      val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
   34.77        (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
   34.78 -    val th2 = equal_elim th1 th
   34.79 +    val th2 = Thm.equal_elim th1 th
   34.80   in
   34.81   (th2, filter_out restricted (!tc_list))
   34.82   end;
    35.1 --- a/src/HOL/Tools/TFL/tfl.ML	Sat May 15 21:41:32 2010 +0200
    35.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Sat May 15 21:50:05 2010 +0200
    35.3 @@ -556,8 +556,8 @@
    35.4                             else ()
    35.5       val f_free = Free (fid, fastype_of f)  (*'cos f is a Const*)
    35.6       val SV' = map tych SV;
    35.7 -     val SVrefls = map reflexive SV'
    35.8 -     val def0 = (fold (fn x => fn th => R.rbeta(combination th x))
    35.9 +     val SVrefls = map Thm.reflexive SV'
   35.10 +     val def0 = (fold (fn x => fn th => R.rbeta(Thm.combination th x))
   35.11                     SVrefls def)
   35.12                  RS meta_eq_to_obj_eq
   35.13       val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0
    36.1 --- a/src/HOL/Tools/choice_specification.ML	Sat May 15 21:41:32 2010 +0200
    36.2 +++ b/src/HOL/Tools/choice_specification.ML	Sat May 15 21:50:05 2010 +0200
    36.3 @@ -183,7 +183,7 @@
    36.4                  fun process_single ((name,atts),rew_imp,frees) args =
    36.5                      let
    36.6                          fun undo_imps thm =
    36.7 -                            equal_elim (symmetric rew_imp) thm
    36.8 +                            Thm.equal_elim (Thm.symmetric rew_imp) thm
    36.9  
   36.10                          fun add_final (arg as (thy, thm)) =
   36.11                              if name = ""
    37.1 --- a/src/HOL/Tools/cnf_funcs.ML	Sat May 15 21:41:32 2010 +0200
    37.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Sat May 15 21:50:05 2010 +0200
    37.3 @@ -435,9 +435,9 @@
    37.4  					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
    37.5  					val var  = new_free ()
    37.6  					val thm2 = make_cnfx_disj_thm (betapply (x', var)) y'  (* (x' | y') = body' *)
    37.7 -					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
    37.8 -					val thm4 = Thm.strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
    37.9 -					val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
   37.10 +					val thm3 = Thm.forall_intr (cterm_of thy var) thm2     (* !!v. (x' | y') = body' *)
   37.11 +					val thm4 = Thm.strip_shyps (thm3 COMP allI)            (* ALL v. (x' | y') = body' *)
   37.12 +					val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
   37.13  				in
   37.14  					iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
   37.15  				end
   37.16 @@ -446,9 +446,9 @@
   37.17  					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
   37.18  					val var  = new_free ()
   37.19  					val thm2 = make_cnfx_disj_thm x' (betapply (y', var))  (* (x' | y') = body' *)
   37.20 -					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
   37.21 -					val thm4 = Thm.strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
   37.22 -					val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
   37.23 +					val thm3 = Thm.forall_intr (cterm_of thy var) thm2     (* !!v. (x' | y') = body' *)
   37.24 +					val thm4 = Thm.strip_shyps (thm3 COMP allI)            (* ALL v. (x' | y') = body' *)
   37.25 +					val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
   37.26  				in
   37.27  					iff_trans OF [thm1, thm5]  (* (x' | (Ex y')) = (EX v. body') *)
   37.28  				end
   37.29 @@ -466,8 +466,8 @@
   37.30  			val var  = new_free ()
   37.31  			val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
   37.32  			val thm2 = make_cnfx_thm_from_nnf body              (* (x | v) & (y | ~v) = body' *)
   37.33 -			val thm3 = forall_intr (cterm_of thy var) thm2      (* !!v. (x | v) & (y | ~v) = body' *)
   37.34 -			val thm4 = Thm.strip_shyps (thm3 COMP allI)             (* ALL v. (x | v) & (y | ~v) = body' *)
   37.35 +			val thm3 = Thm.forall_intr (cterm_of thy var) thm2  (* !!v. (x | v) & (y | ~v) = body' *)
   37.36 +			val thm4 = Thm.strip_shyps (thm3 COMP allI)         (* ALL v. (x | v) & (y | ~v) = body' *)
   37.37  			val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong)  (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
   37.38  		in
   37.39  			iff_trans OF [thm1, thm5]
    38.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat May 15 21:41:32 2010 +0200
    38.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat May 15 21:50:05 2010 +0200
    38.3 @@ -21,7 +21,7 @@
    38.4      [name] => name
    38.5    | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
    38.6  
    38.7 -val all_simps = map (symmetric o mk_meta_eq) @{thms HOL.all_simps};
    38.8 +val all_simps = map (Thm.symmetric o mk_meta_eq) @{thms HOL.all_simps};
    38.9  
   38.10  fun prf_of thm =
   38.11    let
    39.1 --- a/src/HOL/Tools/inductive_set.ML	Sat May 15 21:41:32 2010 +0200
    39.2 +++ b/src/HOL/Tools/inductive_set.ML	Sat May 15 21:50:05 2010 +0200
    39.3 @@ -114,9 +114,9 @@
    39.4              let val rews = map mk_rew ts
    39.5              in
    39.6                if forall is_none rews then NONE
    39.7 -              else SOME (fold (fn th1 => fn th2 => combination th2 th1)
    39.8 -                (map2 (fn SOME r => K r | NONE => reflexive o cterm_of thy)
    39.9 -                   rews ts) (reflexive (cterm_of thy h)))
   39.10 +              else SOME (fold (fn th1 => fn th2 => Thm.combination th2 th1)
   39.11 +                (map2 (fn SOME r => K r | NONE => Thm.reflexive o cterm_of thy)
   39.12 +                   rews ts) (Thm.reflexive (cterm_of thy h)))
   39.13              end
   39.14          | NONE => NONE)
   39.15        | _ => NONE
    40.1 --- a/src/HOL/Tools/int_arith.ML	Sat May 15 21:41:32 2010 +0200
    40.2 +++ b/src/HOL/Tools/int_arith.ML	Sat May 15 21:50:05 2010 +0200
    40.3 @@ -21,7 +21,7 @@
    40.4     That is, m and n consist only of 1s combined with "+", "-" and "*".
    40.5  *)
    40.6  
    40.7 -val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0};
    40.8 +val zeroth = (Thm.symmetric o mk_meta_eq) @{thm of_int_0};
    40.9  
   40.10  val lhss0 = [@{cpat "0::?'a::ring"}];
   40.11  
   40.12 @@ -35,7 +35,7 @@
   40.13    make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
   40.14    proc = proc0, identifier = []};
   40.15  
   40.16 -val oneth = (symmetric o mk_meta_eq) @{thm of_int_1};
   40.17 +val oneth = (Thm.symmetric o mk_meta_eq) @{thm of_int_1};
   40.18  
   40.19  val lhss1 = [@{cpat "1::?'a::ring_1"}];
   40.20  
    41.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Sat May 15 21:41:32 2010 +0200
    41.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Sat May 15 21:50:05 2010 +0200
    41.3 @@ -614,12 +614,12 @@
    41.4  
    41.5   fun prove_nz ss T t =
    41.6      let
    41.7 -      val z = instantiate_cterm ([(zT,T)],[]) zr
    41.8 -      val eq = instantiate_cterm ([(eqT,T)],[]) geq
    41.9 +      val z = Thm.instantiate_cterm ([(zT,T)],[]) zr
   41.10 +      val eq = Thm.instantiate_cterm ([(eqT,T)],[]) geq
   41.11        val th = Simplifier.rewrite (ss addsimps @{thms simp_thms})
   41.12             (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
   41.13                    (Thm.capply (Thm.capply eq t) z)))
   41.14 -    in equal_elim (symmetric th) TrueI
   41.15 +    in Thm.equal_elim (Thm.symmetric th) TrueI
   41.16      end
   41.17  
   41.18   fun proc phi ss ct =
   41.19 @@ -630,7 +630,7 @@
   41.20      val T = ctyp_of_term x
   41.21      val [y_nz, z_nz] = map (prove_nz ss T) [y, z]
   41.22      val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
   41.23 -  in SOME (implies_elim (implies_elim th y_nz) z_nz)
   41.24 +  in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz)
   41.25    end
   41.26    handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
   41.27  
   41.28 @@ -643,13 +643,13 @@
   41.29          let val (x,y) = Thm.dest_binop l val z = r
   41.30              val _ = map (HOLogic.dest_number o term_of) [x,y,z]
   41.31              val ynz = prove_nz ss T y
   41.32 -        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
   41.33 +        in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
   41.34          end
   41.35       | (_, Const (@{const_name Rings.divide},_)$_$_) =>
   41.36          let val (x,y) = Thm.dest_binop r val z = l
   41.37              val _ = map (HOLogic.dest_number o term_of) [x,y,z]
   41.38              val ynz = prove_nz ss T y
   41.39 -        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
   41.40 +        in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
   41.41          end
   41.42       | _ => NONE)
   41.43    end
    42.1 --- a/src/HOL/Tools/record.ML	Sat May 15 21:41:32 2010 +0200
    42.2 +++ b/src/HOL/Tools/record.ML	Sat May 15 21:50:05 2010 +0200
    42.3 @@ -2171,7 +2171,7 @@
    42.4  
    42.5      fun get_upd_acc_congs () =
    42.6        let
    42.7 -        val symdefs = map symmetric (sel_defs @ upd_defs);
    42.8 +        val symdefs = map Thm.symmetric (sel_defs @ upd_defs);
    42.9          val fold_ss = HOL_basic_ss addsimps symdefs;
   42.10          val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists;
   42.11        in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
   42.12 @@ -2257,17 +2257,17 @@
   42.13          val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l);
   42.14          val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r);
   42.15          val thl =
   42.16 -          assume cl                   (*All r. P r*) (* 1 *)
   42.17 -          |> obj_to_meta_all          (*!!r. P r*)
   42.18 -          |> equal_elim split_meta'   (*!!n m more. P (ext n m more)*)
   42.19 -          |> meta_to_obj_all          (*All n m more. P (ext n m more)*) (* 2*)
   42.20 -          |> implies_intr cl          (* 1 ==> 2 *)
   42.21 +          Thm.assume cl                   (*All r. P r*) (* 1 *)
   42.22 +          |> obj_to_meta_all              (*!!r. P r*)
   42.23 +          |> Thm.equal_elim split_meta'   (*!!n m more. P (ext n m more)*)
   42.24 +          |> meta_to_obj_all              (*All n m more. P (ext n m more)*) (* 2*)
   42.25 +          |> Thm.implies_intr cl          (* 1 ==> 2 *)
   42.26          val thr =
   42.27 -          assume cr                             (*All n m more. P (ext n m more)*)
   42.28 -          |> obj_to_meta_all                    (*!!n m more. P (ext n m more)*)
   42.29 -          |> equal_elim (symmetric split_meta') (*!!r. P r*)
   42.30 -          |> meta_to_obj_all                    (*All r. P r*)
   42.31 -          |> implies_intr cr                    (* 2 ==> 1 *)
   42.32 +          Thm.assume cr                                 (*All n m more. P (ext n m more)*)
   42.33 +          |> obj_to_meta_all                            (*!!n m more. P (ext n m more)*)
   42.34 +          |> Thm.equal_elim (Thm.symmetric split_meta') (*!!r. P r*)
   42.35 +          |> meta_to_obj_all                            (*All r. P r*)
   42.36 +          |> Thm.implies_intr cr                        (* 2 ==> 1 *)
   42.37       in thr COMP (thl COMP iffI) end;
   42.38  
   42.39  
    43.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Sat May 15 21:41:32 2010 +0200
    43.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Sat May 15 21:50:05 2010 +0200
    43.3 @@ -147,7 +147,7 @@
    43.4        val semiring = (sr_ops, sr_rules');
    43.5        val ring = (r_ops, r_rules');
    43.6        val field = (f_ops, f_rules');
    43.7 -      val ideal' = map (symmetric o mk_meta) ideal
    43.8 +      val ideal' = map (Thm.symmetric o mk_meta) ideal
    43.9      in
   43.10        AList.delete Thm.eq_thm key #>
   43.11        cons (key, ({vars = vars, semiring = semiring, 
   43.12 @@ -328,16 +328,16 @@
   43.13           ((let val (rx,rn) = dest_pow r
   43.14                 val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29
   43.15                  val (tm1,tm2) = Thm.dest_comb(concl th1) in
   43.16 -               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   43.17 +               Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   43.18             handle CTERM _ =>
   43.19              (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31
   43.20                   val (tm1,tm2) = Thm.dest_comb(concl th1) in
   43.21 -               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
   43.22 +               Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
   43.23         handle CTERM _ =>
   43.24             ((let val (rx,rn) = dest_pow r
   43.25                  val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30
   43.26                  val (tm1,tm2) = Thm.dest_comb(concl th1) in
   43.27 -               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   43.28 +               Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   43.29             handle CTERM _ => inst_thm [(cx,l)] pthm_32
   43.30  
   43.31  ))
   43.32 @@ -348,7 +348,7 @@
   43.33   fun monomial_deone th =
   43.34         (let val (l,r) = dest_mul(concl th) in
   43.35             if l aconvc one_tm
   43.36 -          then transitive th (inst_thm [(ca,r)] pthm_13)  else th end)
   43.37 +          then Thm.transitive th (inst_thm [(ca,r)] pthm_13)  else th end)
   43.38         handle CTERM _ => th;
   43.39  
   43.40  (* Conversion for "(monomial)^n", where n is a numeral.                      *)
   43.41 @@ -357,7 +357,7 @@
   43.42    let
   43.43     fun monomial_pow tm bod ntm =
   43.44      if not(is_comb bod)
   43.45 -    then reflexive tm
   43.46 +    then Thm.reflexive tm
   43.47      else
   43.48       if is_semiring_constant bod
   43.49       then semiring_pow_conv tm
   43.50 @@ -365,7 +365,7 @@
   43.51        let
   43.52        val (lopr,r) = Thm.dest_comb bod
   43.53        in if not(is_comb lopr)
   43.54 -         then reflexive tm
   43.55 +         then Thm.reflexive tm
   43.56          else
   43.57            let
   43.58            val (opr,l) = Thm.dest_comb lopr
   43.59 @@ -374,7 +374,7 @@
   43.60            then
   43.61              let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
   43.62                  val (l,r) = Thm.dest_comb(concl th1)
   43.63 -           in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
   43.64 +           in Thm.transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
   43.65             end
   43.66             else
   43.67              if opr aconvc mul_tm
   43.68 @@ -385,9 +385,9 @@
   43.69                val (x,y) = Thm.dest_comb xy
   43.70                val thl = monomial_pow y l ntm
   43.71                val thr = monomial_pow z r ntm
   43.72 -             in transitive th1 (combination (Drule.arg_cong_rule x thl) thr)
   43.73 +             in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule x thl) thr)
   43.74               end
   43.75 -             else reflexive tm
   43.76 +             else Thm.reflexive tm
   43.77            end
   43.78        end
   43.79    in fn tm =>
   43.80 @@ -436,18 +436,18 @@
   43.81               val (tm1,tm2) = Thm.dest_comb(concl th1)
   43.82               val (tm3,tm4) = Thm.dest_comb tm1
   43.83               val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   43.84 -             val th3 = transitive th1 th2
   43.85 +             val th3 = Thm.transitive th1 th2
   43.86                val  (tm5,tm6) = Thm.dest_comb(concl th3)
   43.87                val  (tm7,tm8) = Thm.dest_comb tm6
   43.88               val  th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8
   43.89 -         in  transitive th3 (Drule.arg_cong_rule tm5 th4)
   43.90 +         in Thm.transitive th3 (Drule.arg_cong_rule tm5 th4)
   43.91           end
   43.92           else
   43.93            let val th0 = if ord < 0 then pthm_16 else pthm_17
   43.94               val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0
   43.95               val (tm1,tm2) = Thm.dest_comb(concl th1)
   43.96               val (tm3,tm4) = Thm.dest_comb tm2
   43.97 -         in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   43.98 +         in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   43.99           end
  43.100          end)
  43.101         handle CTERM _ =>
  43.102 @@ -459,14 +459,14 @@
  43.103                   val (tm1,tm2) = Thm.dest_comb(concl th1)
  43.104             val (tm3,tm4) = Thm.dest_comb tm1
  43.105             val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
  43.106 -          in transitive th1 th2
  43.107 +          in Thm.transitive th1 th2
  43.108            end
  43.109            else
  43.110            if ord < 0 then
  43.111              let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19
  43.112                  val (tm1,tm2) = Thm.dest_comb(concl th1)
  43.113                  val (tm3,tm4) = Thm.dest_comb tm2
  43.114 -           in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
  43.115 +           in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
  43.116             end
  43.117             else inst_thm [(ca,l),(cb,r)] pthm_09
  43.118          end)) end)
  43.119 @@ -480,22 +480,22 @@
  43.120                let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21
  43.121                   val (tm1,tm2) = Thm.dest_comb(concl th1)
  43.122                   val (tm3,tm4) = Thm.dest_comb tm1
  43.123 -             in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
  43.124 +             in Thm.transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
  43.125               end
  43.126               else if ord > 0 then
  43.127                   let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22
  43.128                       val (tm1,tm2) = Thm.dest_comb(concl th1)
  43.129                      val (tm3,tm4) = Thm.dest_comb tm2
  43.130 -                in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
  43.131 +                in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
  43.132                  end
  43.133 -             else reflexive tm
  43.134 +             else Thm.reflexive tm
  43.135           end)
  43.136          handle CTERM _ =>
  43.137            (let val vr = powvar r
  43.138                 val  ord = vorder vl vr
  43.139            in if ord = 0 then powvar_mul_conv tm
  43.140                else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09
  43.141 -              else reflexive tm
  43.142 +              else Thm.reflexive tm
  43.143            end)) end))
  43.144    in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r)
  43.145               end
  43.146 @@ -511,8 +511,8 @@
  43.147            val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37
  43.148            val (tm1,tm2) = Thm.dest_comb(concl th1)
  43.149            val (tm3,tm4) = Thm.dest_comb tm1
  43.150 -          val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
  43.151 -      in transitive th1 th2
  43.152 +          val th2 = Thm.combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
  43.153 +      in Thm.transitive th1 th2
  43.154        end)
  43.155       handle CTERM _ => monomial_mul_conv tm)
  43.156     end
  43.157 @@ -537,11 +537,11 @@
  43.158           val (tm1,tm2) = Thm.dest_comb(concl th1)
  43.159           val (tm3,tm4) = Thm.dest_comb tm1
  43.160           val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4)
  43.161 -         val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2)
  43.162 +         val th3 = Thm.transitive th1 (Drule.fun_cong_rule th2 tm2)
  43.163           val tm5 = concl th3
  43.164        in
  43.165        if (Thm.dest_arg1 tm5) aconvc zero_tm
  43.166 -      then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
  43.167 +      then Thm.transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
  43.168        else monomial_deone th3
  43.169       end
  43.170   end;
  43.171 @@ -603,9 +603,9 @@
  43.172         val l = Thm.dest_arg lopr
  43.173     in
  43.174      if l aconvc zero_tm
  43.175 -    then transitive th (inst_thm [(ca,r)] pthm_07)   else
  43.176 +    then Thm.transitive th (inst_thm [(ca,r)] pthm_07)   else
  43.177          if r aconvc zero_tm
  43.178 -        then transitive th (inst_thm [(ca,l)] pthm_08)  else th
  43.179 +        then Thm.transitive th (inst_thm [(ca,l)] pthm_08)  else th
  43.180     end
  43.181    end
  43.182   fun padd tm =
  43.183 @@ -628,14 +628,14 @@
  43.184              val (tm1,tm2) = Thm.dest_comb(concl th1)
  43.185              val (tm3,tm4) = Thm.dest_comb tm1
  43.186              val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4)
  43.187 -        in dezero_rule (transitive th1 (combination th2 (padd tm2)))
  43.188 +        in dezero_rule (Thm.transitive th1 (Thm.combination th2 (padd tm2)))
  43.189          end
  43.190         else (* ord <> 0*)
  43.191          let val th1 =
  43.192                  if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
  43.193                  else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
  43.194              val (tm1,tm2) = Thm.dest_comb(concl th1)
  43.195 -        in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
  43.196 +        in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
  43.197          end
  43.198        end
  43.199       else (* not (is_add r)*)
  43.200 @@ -646,13 +646,13 @@
  43.201              val (tm1,tm2) = Thm.dest_comb(concl th1)
  43.202              val (tm3,tm4) = Thm.dest_comb tm1
  43.203              val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
  43.204 -        in dezero_rule (transitive th1 th2)
  43.205 +        in dezero_rule (Thm.transitive th1 th2)
  43.206          end
  43.207         else (* ord <> 0*)
  43.208          if ord > 0 then
  43.209            let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
  43.210                val (tm1,tm2) = Thm.dest_comb(concl th1)
  43.211 -          in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
  43.212 +          in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
  43.213            end
  43.214          else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
  43.215        end
  43.216 @@ -667,21 +667,21 @@
  43.217               val (tm1,tm2) = Thm.dest_comb(concl th1)
  43.218               val (tm3,tm4) = Thm.dest_comb tm1
  43.219               val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
  43.220 -         in dezero_rule (transitive th1 th2)
  43.221 +         in dezero_rule (Thm.transitive th1 th2)
  43.222           end
  43.223         else
  43.224 -        if ord > 0 then reflexive tm
  43.225 +        if ord > 0 then Thm.reflexive tm
  43.226          else
  43.227           let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
  43.228               val (tm1,tm2) = Thm.dest_comb(concl th1)
  43.229 -         in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
  43.230 +         in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
  43.231           end
  43.232        end
  43.233      else
  43.234       let val ord = morder l r
  43.235       in
  43.236        if ord = 0 then monomial_add_conv tm
  43.237 -      else if ord > 0 then dezero_rule(reflexive tm)
  43.238 +      else if ord > 0 then dezero_rule(Thm.reflexive tm)
  43.239        else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
  43.240       end
  43.241    end
  43.242 @@ -699,7 +699,7 @@
  43.243      else
  43.244       if not(is_add r) then
  43.245        let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09
  43.246 -      in transitive th1 (polynomial_monomial_mul_conv(concl th1))
  43.247 +      in Thm.transitive th1 (polynomial_monomial_mul_conv(concl th1))
  43.248        end
  43.249       else
  43.250         let val (a,b) = dest_add l
  43.251 @@ -707,8 +707,8 @@
  43.252             val (tm1,tm2) = Thm.dest_comb(concl th1)
  43.253             val (tm3,tm4) = Thm.dest_comb tm1
  43.254             val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4)
  43.255 -           val th3 = transitive th1 (combination th2 (pmul tm2))
  43.256 -       in transitive th3 (polynomial_add_conv (concl th3))
  43.257 +           val th3 = Thm.transitive th1 (Thm.combination th2 (pmul tm2))
  43.258 +       in Thm.transitive th3 (polynomial_add_conv (concl th3))
  43.259         end
  43.260     end
  43.261   in fn tm =>
  43.262 @@ -740,9 +740,9 @@
  43.263           let val th1 = num_conv n
  43.264               val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38
  43.265               val (tm1,tm2) = Thm.dest_comb(concl th2)
  43.266 -             val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
  43.267 -             val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
  43.268 -         in transitive th4 (polynomial_mul_conv (concl th4))
  43.269 +             val th3 = Thm.transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
  43.270 +             val th4 = Thm.transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
  43.271 +         in Thm.transitive th4 (polynomial_mul_conv (concl th4))
  43.272           end
  43.273      end
  43.274   in fn tm =>
  43.275 @@ -755,8 +755,8 @@
  43.276     let val (l,r) = Thm.dest_comb tm in
  43.277          if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
  43.278          let val th1 = inst_thm [(cx',r)] neg_mul
  43.279 -            val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
  43.280 -        in transitive th2 (polynomial_monomial_mul_conv (concl th2))
  43.281 +            val th2 = Thm.transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
  43.282 +        in Thm.transitive th2 (polynomial_monomial_mul_conv (concl th2))
  43.283          end
  43.284     end;
  43.285  
  43.286 @@ -767,51 +767,52 @@
  43.287        val th1 = inst_thm [(cx',l),(cy',r)] sub_add
  43.288        val (tm1,tm2) = Thm.dest_comb(concl th1)
  43.289        val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2)
  43.290 -  in transitive th1 (transitive th2 (polynomial_add_conv (concl th2)))
  43.291 +  in Thm.transitive th1 (Thm.transitive th2 (polynomial_add_conv (concl th2)))
  43.292    end;
  43.293  
  43.294  (* Conversion from HOL term.                                                 *)
  43.295  
  43.296  fun polynomial_conv tm =
  43.297   if is_semiring_constant tm then semiring_add_conv tm
  43.298 - else if not(is_comb tm) then reflexive tm
  43.299 + else if not(is_comb tm) then Thm.reflexive tm
  43.300   else
  43.301    let val (lopr,r) = Thm.dest_comb tm
  43.302    in if lopr aconvc neg_tm then
  43.303         let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
  43.304 -       in transitive th1 (polynomial_neg_conv (concl th1))
  43.305 +       in Thm.transitive th1 (polynomial_neg_conv (concl th1))
  43.306         end
  43.307       else if lopr aconvc inverse_tm then
  43.308         let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
  43.309 -       in transitive th1 (semiring_mul_conv (concl th1))
  43.310 +       in Thm.transitive th1 (semiring_mul_conv (concl th1))
  43.311         end
  43.312       else
  43.313 -       if not(is_comb lopr) then reflexive tm
  43.314 +       if not(is_comb lopr) then Thm.reflexive tm
  43.315         else
  43.316           let val (opr,l) = Thm.dest_comb lopr
  43.317           in if opr aconvc pow_tm andalso is_numeral r
  43.318              then
  43.319                let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
  43.320 -              in transitive th1 (polynomial_pow_conv (concl th1))
  43.321 +              in Thm.transitive th1 (polynomial_pow_conv (concl th1))
  43.322                end
  43.323           else if opr aconvc divide_tm 
  43.324              then
  43.325 -              let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) 
  43.326 +              let val th1 = Thm.combination (Drule.arg_cong_rule opr (polynomial_conv l)) 
  43.327                                          (polynomial_conv r)
  43.328                    val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv)
  43.329                                (Thm.rhs_of th1)
  43.330 -              in transitive th1 th2
  43.331 +              in Thm.transitive th1 th2
  43.332                end
  43.333              else
  43.334                if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
  43.335                then
  43.336 -               let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
  43.337 +               let val th1 =
  43.338 +                    Thm.combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
  43.339                     val f = if opr aconvc add_tm then polynomial_add_conv
  43.340                        else if opr aconvc mul_tm then polynomial_mul_conv
  43.341                        else polynomial_sub_conv
  43.342 -               in transitive th1 (f (concl th1))
  43.343 +               in Thm.transitive th1 (f (concl th1))
  43.344                 end
  43.345 -              else reflexive tm
  43.346 +              else Thm.reflexive tm
  43.347           end
  43.348    end;
  43.349   in
  43.350 @@ -852,7 +853,7 @@
  43.351  
  43.352  fun semiring_normalize_ord_conv ctxt ord tm =
  43.353    (case match ctxt tm of
  43.354 -    NONE => reflexive tm
  43.355 +    NONE => Thm.reflexive tm
  43.356    | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
  43.357   
  43.358  fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
    44.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Sat May 15 21:41:32 2010 +0200
    44.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sat May 15 21:50:05 2010 +0200
    44.3 @@ -845,8 +845,8 @@
    44.4        (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) [neq] of
    44.5          SOME spl =>
    44.6            let val (ct1, ct2) = extract (cprop_of spl)
    44.7 -              val thm1 = assume ct1
    44.8 -              val thm2 = assume ct2
    44.9 +              val thm1 = Thm.assume ct1
   44.10 +              val thm2 = Thm.assume ct2
   44.11            in Spl (spl, ct1, elim_neq neqs (asms', asms@[thm1]),
   44.12              ct2, elim_neq neqs (asms', asms@[thm2]))
   44.13            end
   44.14 @@ -858,8 +858,8 @@
   44.15        let
   44.16          val (thm1, js1) = fwdproof ss tree1 js
   44.17          val (thm2, js2) = fwdproof ss tree2 js1
   44.18 -        val thm1' = implies_intr ct1 thm1
   44.19 -        val thm2' = implies_intr ct2 thm2
   44.20 +        val thm1' = Thm.implies_intr ct1 thm1
   44.21 +        val thm2' = Thm.implies_intr ct2 thm2
   44.22        in (thm2' COMP (thm1' COMP thm), js2) end;
   44.23        (* FIXME needs handle THM _ => NONE ? *)
   44.24  
   44.25 @@ -869,11 +869,11 @@
   44.26      val thy = ProofContext.theory_of ctxt
   44.27      val nTconcl = LA_Logic.neg_prop Tconcl
   44.28      val cnTconcl = cterm_of thy nTconcl
   44.29 -    val nTconclthm = assume cnTconcl
   44.30 +    val nTconclthm = Thm.assume cnTconcl
   44.31      val tree = (if split_neq then splitasms ctxt else Tip) (thms @ [nTconclthm])
   44.32      val (Falsethm, _) = fwdproof ss tree js
   44.33      val contr = if pos then LA_Logic.ccontr else LA_Logic.notI
   44.34 -    val concl = implies_intr cnTconcl Falsethm COMP contr
   44.35 +    val concl = Thm.implies_intr cnTconcl Falsethm COMP contr
   44.36    in SOME (trace_thm ctxt "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end
   44.37    (*in case concl contains ?-var, which makes assume fail:*)   (* FIXME Variable.import_terms *)
   44.38    handle THM _ => NONE;
    45.1 --- a/src/Provers/hypsubst.ML	Sat May 15 21:41:32 2010 +0200
    45.2 +++ b/src/Provers/hypsubst.ML	Sat May 15 21:50:05 2010 +0200
    45.3 @@ -143,7 +143,7 @@
    45.4      [ if inspect_pair bnd false (Data.dest_eq
    45.5                                     (Data.dest_Trueprop (#prop (rep_thm th))))
    45.6        then th RS Data.eq_reflection
    45.7 -      else symmetric(th RS Data.eq_reflection) (*reorient*) ]
    45.8 +      else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
    45.9      handle TERM _ => [] | Match => [];
   45.10  
   45.11  local
    46.1 --- a/src/Tools/Compute_Oracle/compute.ML	Sat May 15 21:41:32 2010 +0200
    46.2 +++ b/src/Tools/Compute_Oracle/compute.ML	Sat May 15 21:50:05 2010 +0200
    46.3 @@ -391,9 +391,9 @@
    46.4  fun export_thm thy hyps shyps prop =
    46.5      let
    46.6          val th = export_oracle (thy, hyps, shyps, prop)
    46.7 -        val hyps = map (fn h => assume (cterm_of thy h)) hyps
    46.8 +        val hyps = map (fn h => Thm.assume (cterm_of thy h)) hyps
    46.9      in
   46.10 -        fold (fn h => fn p => implies_elim p h) hyps th 
   46.11 +        fold (fn h => fn p => Thm.implies_elim p h) hyps th 
   46.12      end
   46.13          
   46.14  (* --------- Rewrite ----------- *)
    47.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Sat May 15 21:41:32 2010 +0200
    47.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Sat May 15 21:50:05 2010 +0200
    47.3 @@ -54,13 +54,13 @@
    47.4  
    47.5  (* beta contract the theorem *)
    47.6  fun beta_contract thm = 
    47.7 -    equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
    47.8 +    Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
    47.9  
   47.10  (* beta-eta contract the theorem *)
   47.11  fun beta_eta_contract thm = 
   47.12      let
   47.13 -      val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
   47.14 -      val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
   47.15 +      val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
   47.16 +      val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
   47.17      in thm3 end;
   47.18  
   47.19  
    48.1 --- a/src/Tools/coherent.ML	Sat May 15 21:41:32 2010 +0200
    48.2 +++ b/src/Tools/coherent.ML	Sat May 15 21:50:05 2010 +0200
    48.3 @@ -46,8 +46,8 @@
    48.4  fun rulify_elim_conv ct =
    48.5    if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct
    48.6    else concl_conv (length (Logic.strip_imp_prems (term_of ct)))
    48.7 -    (rewr_conv (symmetric Data.atomize_elimL) then_conv
    48.8 -     MetaSimplifier.rewrite true (map symmetric
    48.9 +    (rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
   48.10 +     MetaSimplifier.rewrite true (map Thm.symmetric
   48.11         [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
   48.12  
   48.13  end;
    49.1 --- a/src/ZF/Tools/induct_tacs.ML	Sat May 15 21:41:32 2010 +0200
    49.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sat May 15 21:50:05 2010 +0200
    49.3 @@ -89,7 +89,7 @@
    49.4  fun exhaust_induct_tac exh ctxt var i state =
    49.5    let
    49.6      val thy = ProofContext.theory_of ctxt
    49.7 -    val (_, _, Bi, _) = dest_state (state, i)
    49.8 +    val (_, _, Bi, _) = Thm.dest_state (state, i)
    49.9      val tn = find_tname var Bi
   49.10      val rule =
   49.11          if exh then #exhaustion (datatype_info thy tn)