less pervasive names from structure Thm;
authorwenzelm
Sat May 15 21:41:32 2010 +0200 (2010-05-15)
changeset 36944dbf831a50e4a
parent 36943 ae740b96b914
child 36945 9bec62c10714
less pervasive names from structure Thm;
src/Pure/drule.ML
src/Pure/meta_simplifier.ML
src/Pure/old_goals.ML
src/Pure/tactic.ML
     1.1 --- a/src/Pure/drule.ML	Sat May 15 21:09:54 2010 +0200
     1.2 +++ b/src/Pure/drule.ML	Sat May 15 21:41:32 2010 +0200
     1.3 @@ -204,11 +204,11 @@
     1.4  (** Standardization of rules **)
     1.5  
     1.6  (*Generalization over a list of variables*)
     1.7 -val forall_intr_list = fold_rev forall_intr;
     1.8 +val forall_intr_list = fold_rev Thm.forall_intr;
     1.9  
    1.10  (*Generalization over Vars -- canonical order*)
    1.11  fun forall_intr_vars th =
    1.12 -  fold forall_intr
    1.13 +  fold Thm.forall_intr
    1.14      (map (Thm.cterm_of (Thm.theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th [])) th;
    1.15  
    1.16  fun outer_params t =
    1.17 @@ -245,10 +245,10 @@
    1.18  fun generalize names th = Thm.generalize names (Thm.maxidx_of th + 1) th;
    1.19  
    1.20  (*specialization over a list of cterms*)
    1.21 -val forall_elim_list = fold forall_elim;
    1.22 +val forall_elim_list = fold Thm.forall_elim;
    1.23  
    1.24  (*maps A1,...,An |- B  to  [| A1;...;An |] ==> B*)
    1.25 -val implies_intr_list = fold_rev implies_intr;
    1.26 +val implies_intr_list = fold_rev Thm.implies_intr;
    1.27  
    1.28  (*maps [| A1;...;An |] ==> B and [A1,...,An]  to  B*)
    1.29  fun implies_elim_list impth ths = fold Thm.elim_implies ths impth;
    1.30 @@ -278,7 +278,7 @@
    1.31    This step can lose information.*)
    1.32  fun flexflex_unique th =
    1.33    if null (tpairs_of th) then th else
    1.34 -    case distinct Thm.eq_thm (Seq.list_of (flexflex_rule th)) of
    1.35 +    case distinct Thm.eq_thm (Seq.list_of (Thm.flexflex_rule th)) of
    1.36        [th] => th
    1.37      | []   => raise THM("flexflex_unique: impossible constraints", 0, [th])
    1.38      |  _   => raise THM("flexflex_unique: multiple unifiers", 0, [th]);
    1.39 @@ -464,8 +464,8 @@
    1.40  
    1.41  fun extensional eq =
    1.42    let val eq' =
    1.43 -    abstract_rule "x" (Thm.dest_arg (fst (Thm.dest_equals (cprop_of eq)))) eq
    1.44 -  in equal_elim (eta_conversion (cprop_of eq')) eq' end;
    1.45 +    Thm.abstract_rule "x" (Thm.dest_arg (fst (Thm.dest_equals (cprop_of eq)))) eq
    1.46 +  in Thm.equal_elim (Thm.eta_conversion (cprop_of eq')) eq' end;
    1.47  
    1.48  val equals_cong =
    1.49    store_standard_thm_open (Binding.name "equals_cong")
    1.50 @@ -478,13 +478,13 @@
    1.51      val AC = read_prop "A ==> C"
    1.52      val A = read_prop "A"
    1.53    in
    1.54 -    store_standard_thm_open (Binding.name "imp_cong") (implies_intr ABC (equal_intr
    1.55 -      (implies_intr AB (implies_intr A
    1.56 -        (equal_elim (implies_elim (assume ABC) (assume A))
    1.57 -          (implies_elim (assume AB) (assume A)))))
    1.58 -      (implies_intr AC (implies_intr A
    1.59 -        (equal_elim (symmetric (implies_elim (assume ABC) (assume A)))
    1.60 -          (implies_elim (assume AC) (assume A)))))))
    1.61 +    store_standard_thm_open (Binding.name "imp_cong") (Thm.implies_intr ABC (Thm.equal_intr
    1.62 +      (Thm.implies_intr AB (Thm.implies_intr A
    1.63 +        (Thm.equal_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A))
    1.64 +          (Thm.implies_elim (Thm.assume AB) (Thm.assume A)))))
    1.65 +      (Thm.implies_intr AC (Thm.implies_intr A
    1.66 +        (Thm.equal_elim (Thm.symmetric (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)))
    1.67 +          (Thm.implies_elim (Thm.assume AC) (Thm.assume A)))))))
    1.68    end;
    1.69  
    1.70  val swap_prems_eq =
    1.71 @@ -495,11 +495,11 @@
    1.72      val B = read_prop "B"
    1.73    in
    1.74      store_standard_thm_open (Binding.name "swap_prems_eq")
    1.75 -      (equal_intr
    1.76 -        (implies_intr ABC (implies_intr B (implies_intr A
    1.77 -          (implies_elim (implies_elim (assume ABC) (assume A)) (assume B)))))
    1.78 -        (implies_intr BAC (implies_intr A (implies_intr B
    1.79 -          (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
    1.80 +      (Thm.equal_intr
    1.81 +        (Thm.implies_intr ABC (Thm.implies_intr B (Thm.implies_intr A
    1.82 +          (Thm.implies_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)) (Thm.assume B)))))
    1.83 +        (Thm.implies_intr BAC (Thm.implies_intr A (Thm.implies_intr B
    1.84 +          (Thm.implies_elim (Thm.implies_elim (Thm.assume BAC) (Thm.assume B)) (Thm.assume A))))))
    1.85    end;
    1.86  
    1.87  val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies);
    1.88 @@ -513,16 +513,18 @@
    1.89    val rhs_of = snd o dest_eq
    1.90  in
    1.91  fun beta_eta_conversion t =
    1.92 -  let val thm = beta_conversion true t
    1.93 -  in transitive thm (eta_conversion (rhs_of thm)) end
    1.94 +  let val thm = Thm.beta_conversion true t
    1.95 +  in Thm.transitive thm (Thm.eta_conversion (rhs_of thm)) end
    1.96  end;
    1.97  
    1.98 -fun eta_long_conversion ct = transitive (beta_eta_conversion ct)
    1.99 -  (symmetric (beta_eta_conversion (cterm_fun (Pattern.eta_long []) ct)));
   1.100 +fun eta_long_conversion ct =
   1.101 +  Thm.transitive
   1.102 +    (beta_eta_conversion ct)
   1.103 +    (Thm.symmetric (beta_eta_conversion (cterm_fun (Pattern.eta_long []) ct)));
   1.104  
   1.105  (*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*)
   1.106  fun eta_contraction_rule th =
   1.107 -  equal_elim (eta_conversion (cprop_of th)) th;
   1.108 +  Thm.equal_elim (Thm.eta_conversion (cprop_of th)) th;
   1.109  
   1.110  
   1.111  (* abs_def *)
   1.112 @@ -578,7 +580,7 @@
   1.113      val VW = read_prop "V ==> W";
   1.114    in
   1.115      store_standard_thm_open (Binding.name "revcut_rl")
   1.116 -      (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
   1.117 +      (Thm.implies_intr V (Thm.implies_intr VW (Thm.implies_elim (Thm.assume VW) (Thm.assume V))))
   1.118    end;
   1.119  
   1.120  (*for deleting an unwanted assumption*)
   1.121 @@ -586,7 +588,7 @@
   1.122    let
   1.123      val V = read_prop "V";
   1.124      val W = read_prop "W";
   1.125 -    val thm = implies_intr V (implies_intr W (assume W));
   1.126 +    val thm = Thm.implies_intr V (Thm.implies_intr W (Thm.assume W));
   1.127    in store_standard_thm_open (Binding.name "thin_rl") thm end;
   1.128  
   1.129  (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
   1.130 @@ -597,8 +599,8 @@
   1.131      val x = certify (Free ("x", Term.aT []));
   1.132    in
   1.133      store_standard_thm_open (Binding.name "triv_forall_equality")
   1.134 -      (equal_intr (implies_intr QV (forall_elim x (assume QV)))
   1.135 -        (implies_intr V  (forall_intr x (assume V))))
   1.136 +      (Thm.equal_intr (Thm.implies_intr QV (Thm.forall_elim x (Thm.assume QV)))
   1.137 +        (Thm.implies_intr V (Thm.forall_intr x (Thm.assume V))))
   1.138    end;
   1.139  
   1.140  (* (PROP ?Phi ==> PROP ?Phi ==> PROP ?Psi) ==>
   1.141 @@ -610,7 +612,7 @@
   1.142      val A = read_prop "Phi";
   1.143    in
   1.144      store_standard_thm_open (Binding.name "distinct_prems_rl")
   1.145 -      (implies_intr_list [AAB, A] (implies_elim_list (assume AAB) [assume A, assume A]))
   1.146 +      (implies_intr_list [AAB, A] (implies_elim_list (Thm.assume AAB) [Thm.assume A, Thm.assume A]))
   1.147    end;
   1.148  
   1.149  (* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
   1.150 @@ -620,15 +622,15 @@
   1.151  val swap_prems_rl =
   1.152    let
   1.153      val cmajor = read_prop "PhiA ==> PhiB ==> Psi";
   1.154 -    val major = assume cmajor;
   1.155 +    val major = Thm.assume cmajor;
   1.156      val cminor1 = read_prop "PhiA";
   1.157 -    val minor1 = assume cminor1;
   1.158 +    val minor1 = Thm.assume cminor1;
   1.159      val cminor2 = read_prop "PhiB";
   1.160 -    val minor2 = assume cminor2;
   1.161 +    val minor2 = Thm.assume cminor2;
   1.162    in
   1.163      store_standard_thm_open (Binding.name "swap_prems_rl")
   1.164 -      (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   1.165 -        (implies_elim (implies_elim major minor1) minor2))))
   1.166 +      (Thm.implies_intr cmajor (Thm.implies_intr cminor2 (Thm.implies_intr cminor1
   1.167 +        (Thm.implies_elim (Thm.implies_elim major minor1) minor2))))
   1.168    end;
   1.169  
   1.170  (* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
   1.171 @@ -641,7 +643,7 @@
   1.172      val QP = read_prop "psi ==> phi";
   1.173    in
   1.174      store_standard_thm_open (Binding.name "equal_intr_rule")
   1.175 -      (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   1.176 +      (Thm.implies_intr PQ (Thm.implies_intr QP (Thm.equal_intr (Thm.assume PQ) (Thm.assume QP))))
   1.177    end;
   1.178  
   1.179  (* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *)
   1.180 @@ -651,7 +653,7 @@
   1.181      val P = read_prop "phi";
   1.182    in
   1.183      store_standard_thm_open (Binding.name "equal_elim_rule1")
   1.184 -      (Thm.equal_elim (assume eq) (assume P) |> implies_intr_list [eq, P])
   1.185 +      (Thm.equal_elim (Thm.assume eq) (Thm.assume P) |> implies_intr_list [eq, P])
   1.186    end;
   1.187  
   1.188  (* PROP ?psi == PROP ?phi ==> PROP ?phi ==> PROP ?psi *)
   1.189 @@ -917,7 +919,7 @@
   1.190          fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, ren t)
   1.191            | ren (t $ u) = ren t $ ren u
   1.192            | ren t = t;
   1.193 -      in equal_elim (reflexive (cert (ren (Thm.prop_of thm)))) thm end;
   1.194 +      in Thm.equal_elim (Thm.reflexive (cert (ren (Thm.prop_of thm)))) thm end;
   1.195  
   1.196  
   1.197  (* renaming in left-to-right order *)
   1.198 @@ -937,7 +939,7 @@
   1.199            in (xs'', t' $ u') end
   1.200        | rename xs t = (xs, t);
   1.201    in case rename xs prop of
   1.202 -      ([], prop') => equal_elim (reflexive (cert prop')) thm
   1.203 +      ([], prop') => Thm.equal_elim (Thm.reflexive (cert prop')) thm
   1.204      | _ => error "More names than abstractions in theorem"
   1.205    end;
   1.206  
     2.1 --- a/src/Pure/meta_simplifier.ML	Sat May 15 21:09:54 2010 +0200
     2.2 +++ b/src/Pure/meta_simplifier.ML	Sat May 15 21:41:32 2010 +0200
     2.3 @@ -832,9 +832,9 @@
     2.4  
     2.5  fun check_conv msg ss thm thm' =
     2.6    let
     2.7 -    val thm'' = transitive thm thm' handle THM _ =>
     2.8 -     transitive thm (transitive
     2.9 -       (symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
    2.10 +    val thm'' = Thm.transitive thm thm' handle THM _ =>
    2.11 +     Thm.transitive thm (Thm.transitive
    2.12 +       (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
    2.13    in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
    2.14    handle THM _ =>
    2.15      let
    2.16 @@ -972,8 +972,8 @@
    2.17                    | some => some)))
    2.18            else proc_rews ps;
    2.19    in case eta_t of
    2.20 -       Abs _ $ _ => SOME (transitive eta_thm
    2.21 -         (beta_conversion false eta_t'), skel0)
    2.22 +       Abs _ $ _ => SOME (Thm.transitive eta_thm
    2.23 +         (Thm.beta_conversion false eta_t'), skel0)
    2.24       | _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of
    2.25                 NONE => proc_rews (Net.match_term procs eta_t)
    2.26               | some => some)
    2.27 @@ -1006,7 +1006,7 @@
    2.28  fun transitive1 NONE NONE = NONE
    2.29    | transitive1 (SOME thm1) NONE = SOME thm1
    2.30    | transitive1 NONE (SOME thm2) = SOME thm2
    2.31 -  | transitive1 (SOME thm1) (SOME thm2) = SOME (transitive thm1 thm2)
    2.32 +  | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2)
    2.33  
    2.34  fun transitive2 thm = transitive1 (SOME thm);
    2.35  fun transitive3 thm = transitive1 thm o SOME;
    2.36 @@ -1020,7 +1020,7 @@
    2.37               some as SOME thm1 =>
    2.38                 (case rewritec (prover, thy, maxidx) ss (Thm.rhs_of thm1) of
    2.39                    SOME (thm2, skel2) =>
    2.40 -                    transitive2 (transitive thm1 thm2)
    2.41 +                    transitive2 (Thm.transitive thm1 thm2)
    2.42                        (botc skel2 ss (Thm.rhs_of thm2))
    2.43                  | NONE => some)
    2.44             | NONE =>
    2.45 @@ -1031,7 +1031,7 @@
    2.46  
    2.47      and try_botc ss t =
    2.48            (case botc skel0 ss t of
    2.49 -             SOME trec1 => trec1 | NONE => (reflexive t))
    2.50 +             SOME trec1 => trec1 | NONE => (Thm.reflexive t))
    2.51  
    2.52      and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 =
    2.53         (case term_of t0 of
    2.54 @@ -1048,16 +1048,16 @@
    2.55                   val ss' = add_bound ((b', T), a) ss;
    2.56                   val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
    2.57               in case botc skel' ss' t' of
    2.58 -                  SOME thm => SOME (abstract_rule a v thm)
    2.59 +                  SOME thm => SOME (Thm.abstract_rule a v thm)
    2.60                  | NONE => NONE
    2.61               end
    2.62           | t $ _ => (case t of
    2.63               Const ("==>", _) $ _  => impc t0 ss
    2.64             | Abs _ =>
    2.65 -               let val thm = beta_conversion false t0
    2.66 +               let val thm = Thm.beta_conversion false t0
    2.67                 in case subc skel0 ss (Thm.rhs_of thm) of
    2.68                      NONE => SOME thm
    2.69 -                  | SOME thm' => SOME (transitive thm thm')
    2.70 +                  | SOME thm' => SOME (Thm.transitive thm thm')
    2.71                 end
    2.72             | _  =>
    2.73                 let fun appc () =
    2.74 @@ -1070,11 +1070,11 @@
    2.75                       (case botc tskel ss ct of
    2.76                          SOME thm1 =>
    2.77                            (case botc uskel ss cu of
    2.78 -                             SOME thm2 => SOME (combination thm1 thm2)
    2.79 -                           | NONE => SOME (combination thm1 (reflexive cu)))
    2.80 +                             SOME thm2 => SOME (Thm.combination thm1 thm2)
    2.81 +                           | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu)))
    2.82                        | NONE =>
    2.83                            (case botc uskel ss cu of
    2.84 -                             SOME thm1 => SOME (combination (reflexive ct) thm1)
    2.85 +                             SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1)
    2.86                             | NONE => NONE))
    2.87                       end
    2.88                     val (h, ts) = strip_comb t
    2.89 @@ -1095,7 +1095,7 @@
    2.90                             in case botc skel ss cl of
    2.91                                  NONE => thm
    2.92                                | SOME thm' => transitive3 thm
    2.93 -                                  (combination thm' (reflexive cr))
    2.94 +                                  (Thm.combination thm' (Thm.reflexive cr))
    2.95                             end handle Pattern.MATCH => appc ()))
    2.96                    | _ => appc ()
    2.97                 end)
    2.98 @@ -1110,7 +1110,7 @@
    2.99          (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")
   2.100            ss prem; ([], NONE))
   2.101        else
   2.102 -        let val asm = assume prem
   2.103 +        let val asm = Thm.assume prem
   2.104          in (extract_safe_rrules (ss, asm), SOME asm) end
   2.105  
   2.106      and add_rrules (rrss, asms) ss =
   2.107 @@ -1119,14 +1119,14 @@
   2.108      and disch r prem eq =
   2.109        let
   2.110          val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
   2.111 -        val eq' = implies_elim (Thm.instantiate
   2.112 +        val eq' = Thm.implies_elim (Thm.instantiate
   2.113            ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
   2.114 -          (implies_intr prem eq)
   2.115 +          (Thm.implies_intr prem eq)
   2.116        in if not r then eq' else
   2.117          let
   2.118            val (prem', concl) = Thm.dest_implies lhs;
   2.119            val (prem'', _) = Thm.dest_implies rhs
   2.120 -        in transitive (transitive
   2.121 +        in Thm.transitive (Thm.transitive
   2.122            (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
   2.123               Drule.swap_prems_eq) eq')
   2.124            (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
   2.125 @@ -1182,7 +1182,7 @@
   2.126              in mut_impc prems concl rrss asms (prem' :: prems')
   2.127                (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
   2.128                  (take i prems)
   2.129 -                (Drule.imp_cong_rule eqn (reflexive (Drule.list_implies
   2.130 +                (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
   2.131                    (drop i prems, concl))))) :: eqns)
   2.132                    ss (length prems') ~1
   2.133              end
   2.134 @@ -1197,13 +1197,13 @@
   2.135         in (case botc skel0 ss1 conc of
   2.136             NONE => (case thm1 of
   2.137                 NONE => NONE
   2.138 -             | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (reflexive conc)))
   2.139 +             | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (Thm.reflexive conc)))
   2.140           | SOME thm2 =>
   2.141             let val thm2' = disch false prem1 thm2
   2.142             in (case thm1 of
   2.143                 NONE => SOME thm2'
   2.144               | SOME thm1' =>
   2.145 -                 SOME (transitive (Drule.imp_cong_rule thm1' (reflexive conc)) thm2'))
   2.146 +                 SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2'))
   2.147             end)
   2.148         end
   2.149  
   2.150 @@ -1321,7 +1321,7 @@
   2.151        val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
   2.152    in map (AList.find (op =) keylist) keys end;
   2.153  
   2.154 -val rev_defs = sort_lhs_depths o map symmetric;
   2.155 +val rev_defs = sort_lhs_depths o map Thm.symmetric;
   2.156  
   2.157  fun fold_rule defs = fold rewrite_rule (rev_defs defs);
   2.158  fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
     3.1 --- a/src/Pure/old_goals.ML	Sat May 15 21:09:54 2010 +0200
     3.2 +++ b/src/Pure/old_goals.ML	Sat May 15 21:41:32 2010 +0200
     3.3 @@ -134,7 +134,7 @@
     3.4        val maxidx = Thm.maxidx_of state
     3.5        val cterm = Thm.cterm_of (Thm.theory_of_thm state)
     3.6        val chyps = map cterm hyps
     3.7 -      val hypths = map assume chyps
     3.8 +      val hypths = map Thm.assume chyps
     3.9        val subprems = map (Thm.forall_elim_vars 0) hypths
    3.10        val fparams = map Free params
    3.11        val cparams = map cterm fparams
    3.12 @@ -165,7 +165,7 @@
    3.13              val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
    3.14              val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
    3.15              val emBs = map (cterm o embed) (prems_of st')
    3.16 -            val Cth  = implies_elim_list st' (map (elim o assume) emBs)
    3.17 +            val Cth  = implies_elim_list st' (map (elim o Thm.assume) emBs)
    3.18          in  (*restore the unknowns to the hypotheses*)
    3.19              free_instantiate (map swap_ctpair insts @
    3.20                                map mk_subgoal_swap_ctpair subgoal_insts)
    3.21 @@ -175,7 +175,7 @@
    3.22          end
    3.23        (*function to replace the current subgoal*)
    3.24        fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
    3.25 -  in Seq.maps next (tacf subprems (trivial (cterm concl))) end;
    3.26 +  in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
    3.27  
    3.28  end;
    3.29  
    3.30 @@ -308,7 +308,7 @@
    3.31        (*discharges assumptions from state in the order they appear in goal;
    3.32          checks (if requested) that resulting theorem is equivalent to goal. *)
    3.33        fun mkresult (check,state) =
    3.34 -        let val state = Seq.hd (flexflex_rule state)
    3.35 +        let val state = Seq.hd (Thm.flexflex_rule state)
    3.36                          handle THM _ => state   (*smash flexflex pairs*)
    3.37              val ngoals = nprems_of state
    3.38              val ath = implies_intr_list cAs state
    3.39 @@ -522,7 +522,7 @@
    3.40            | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
    3.41    in
    3.42      Drule.export_without_context (implies_intr_list As
    3.43 -      (check (Seq.pull (EVERY (f asms) (trivial B)))))
    3.44 +      (check (Seq.pull (EVERY (f asms) (Thm.trivial B)))))
    3.45    end;
    3.46  
    3.47  
     4.1 --- a/src/Pure/tactic.ML	Sat May 15 21:09:54 2010 +0200
     4.2 +++ b/src/Pure/tactic.ML	Sat May 15 21:41:32 2010 +0200
     4.3 @@ -156,7 +156,7 @@
     4.4  fun dmatch_tac rls   = ematch_tac (map make_elim rls);
     4.5  
     4.6  (*Smash all flex-flex disagreement pairs in the proof state.*)
     4.7 -val flexflex_tac = PRIMSEQ flexflex_rule;
     4.8 +val flexflex_tac = PRIMSEQ Thm.flexflex_rule;
     4.9  
    4.10  (*Remove duplicate subgoals.*)
    4.11  val perm_tac = PRIMITIVE oo Thm.permute_prems;
    4.12 @@ -185,7 +185,7 @@
    4.13  
    4.14  (*Determine print names of goal parameters (reversed)*)
    4.15  fun innermost_params i st =
    4.16 -  let val (_, _, Bi, _) = dest_state (st, i)
    4.17 +  let val (_, _, Bi, _) = Thm.dest_state (st, i)
    4.18    in Term.rename_wrt_term Bi (Logic.strip_params Bi) end;
    4.19  
    4.20