structure Thm: less pervasive names;
authorwenzelm
Mon Jul 06 21:24:30 2009 +0200 (2009-07-06)
changeset 31945d5f186aa0bed
parent 31944 c8a35979a5bc
child 31946 99ac0321cd47
structure Thm: less pervasive names;
src/HOL/Bali/AxCompl.thy
src/HOL/Import/import.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Set.thy
src/HOL/TLA/Intensional.thy
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/metis_tools.ML
src/Provers/blast.ML
src/Provers/classical.ML
src/Pure/Isar/rule_insts.ML
src/Pure/drule.ML
src/Pure/tactic.ML
src/Pure/tctical.ML
src/Pure/thm.ML
src/Tools/IsaPlanner/isand.ML
     1.1 --- a/src/HOL/Bali/AxCompl.thy	Mon Jul 06 20:36:38 2009 +0200
     1.2 +++ b/src/HOL/Bali/AxCompl.thy	Mon Jul 06 21:24:30 2009 +0200
     1.3 @@ -1402,7 +1402,7 @@
     1.4  apply -
     1.5  apply (induct_tac "n")
     1.6  apply  (tactic "ALLGOALS (clarsimp_tac @{clasimpset})")
     1.7 -apply  (tactic {* dtac (permute_prems 0 1 (thm "card_seteq")) 1 *})
     1.8 +apply  (tactic {* dtac (Thm.permute_prems 0 1 (thm "card_seteq")) 1 *})
     1.9  apply    simp
    1.10  apply   (erule finite_imageI)
    1.11  apply  (simp add: MGF_asm ax_derivs_asm)
     2.1 --- a/src/HOL/Import/import.ML	Mon Jul 06 20:36:38 2009 +0200
     2.2 +++ b/src/HOL/Import/import.ML	Mon Jul 06 21:24:30 2009 +0200
     2.3 @@ -55,7 +55,7 @@
     2.4                              then message "import: Terms match up"
     2.5                              else message "import: Terms DO NOT match up"
     2.6                      val thm' = equal_elim (symmetric prew) thm
     2.7 -                    val res = bicompose true (false,thm',0) 1 th
     2.8 +                    val res = Thm.bicompose true (false,thm',0) 1 th
     2.9                  in
    2.10                      res
    2.11                  end
     3.1 --- a/src/HOL/Import/proof_kernel.ML	Mon Jul 06 20:36:38 2009 +0200
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Mon Jul 06 21:24:30 2009 +0200
     3.3 @@ -977,7 +977,7 @@
     3.4  
     3.5  fun uniq_compose m th i st =
     3.6      let
     3.7 -        val res = bicompose false (false,th,m) i st
     3.8 +        val res = Thm.bicompose false (false,th,m) i st
     3.9      in
    3.10          case Seq.pull res of
    3.11              SOME (th,rest) => (case Seq.pull rest of
    3.12 @@ -1065,14 +1065,12 @@
    3.13          res
    3.14      end
    3.15  
    3.16 -val permute_prems = Thm.permute_prems
    3.17 -
    3.18  fun rearrange sg tm th =
    3.19      let
    3.20          val tm' = Envir.beta_eta_contract tm
    3.21 -        fun find []      n = permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
    3.22 +        fun find []      n = Thm.permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
    3.23            | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p)
    3.24 -                             then permute_prems n 1 th
    3.25 +                             then Thm.permute_prems n 1 th
    3.26                               else find ps (n+1)
    3.27      in
    3.28          find (prems_of th) 0
    3.29 @@ -1193,7 +1191,7 @@
    3.30  fun if_debug f x = if !debug then f x else ()
    3.31  val message = if_debug writeln
    3.32  
    3.33 -val conjE_helper = permute_prems 0 1 conjE
    3.34 +val conjE_helper = Thm.permute_prems 0 1 conjE
    3.35  
    3.36  fun get_hol4_thm thyname thmname thy =
    3.37      case get_hol4_theorem thyname thmname thy of
     4.1 --- a/src/HOL/Import/shuffler.ML	Mon Jul 06 20:36:38 2009 +0200
     4.2 +++ b/src/HOL/Import/shuffler.ML	Mon Jul 06 21:24:30 2009 +0200
     4.3 @@ -595,7 +595,7 @@
     4.4                  val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
     4.5                  val triv_th = trivial rhs
     4.6                  val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
     4.7 -                val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
     4.8 +                val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
     4.9                                   SOME(th,_) => SOME th
    4.10                                 | NONE => NONE
    4.11              in
     5.1 --- a/src/HOL/Set.thy	Mon Jul 06 20:36:38 2009 +0200
     5.2 +++ b/src/HOL/Set.thy	Mon Jul 06 21:24:30 2009 +0200
     5.3 @@ -449,7 +449,7 @@
     5.4  lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
     5.5    by (unfold Ball_def) blast
     5.6  
     5.7 -ML {* bind_thm ("rev_ballE", permute_prems 1 1 @{thm ballE}) *}
     5.8 +ML {* bind_thm ("rev_ballE", Thm.permute_prems 1 1 @{thm ballE}) *}
     5.9  
    5.10  text {*
    5.11    \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and
     6.1 --- a/src/HOL/TLA/Intensional.thy	Mon Jul 06 20:36:38 2009 +0200
     6.2 +++ b/src/HOL/TLA/Intensional.thy	Mon Jul 06 21:24:30 2009 +0200
     6.3 @@ -268,7 +268,7 @@
     6.4    let
     6.5      (* analogous to RS, but using matching instead of resolution *)
     6.6      fun matchres tha i thb =
     6.7 -      case Seq.chop 2 (biresolution true [(false,tha)] i thb) of
     6.8 +      case Seq.chop 2 (Thm.biresolution true [(false,tha)] i thb) of
     6.9            ([th],_) => th
    6.10          | ([],_)   => raise THM("matchres: no match", i, [tha,thb])
    6.11          |      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])
     7.1 --- a/src/HOL/Tools/TFL/rules.ML	Mon Jul 06 20:36:38 2009 +0200
     7.2 +++ b/src/HOL/Tools/TFL/rules.ML	Mon Jul 06 21:24:30 2009 +0200
     7.3 @@ -519,14 +519,14 @@
     7.4              handle TERM _ => get (rst, n+1, L)
     7.5                | U.ERR _ => get (rst, n+1, L);
     7.6  
     7.7 -(* Note: rename_params_rule counts from 1, not 0 *)
     7.8 +(* Note: Thm.rename_params_rule counts from 1, not 0 *)
     7.9  fun rename thm =
    7.10    let val thy = Thm.theory_of_thm thm
    7.11        val tych = cterm_of thy
    7.12        val ants = Logic.strip_imp_prems (Thm.prop_of thm)
    7.13        val news = get (ants,1,[])
    7.14    in
    7.15 -  fold rename_params_rule news thm
    7.16 +  fold Thm.rename_params_rule news thm
    7.17    end;
    7.18  
    7.19  
     8.1 --- a/src/HOL/Tools/meson.ML	Mon Jul 06 20:36:38 2009 +0200
     8.2 +++ b/src/HOL/Tools/meson.ML	Mon Jul 06 21:24:30 2009 +0200
     8.3 @@ -470,7 +470,7 @@
     8.4  (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
     8.5  fun TRYING_eq_assume_tac 0 st = Seq.single st
     8.6    | TRYING_eq_assume_tac i st =
     8.7 -       TRYING_eq_assume_tac (i-1) (eq_assumption i st)
     8.8 +       TRYING_eq_assume_tac (i-1) (Thm.eq_assumption i st)
     8.9         handle THM _ => TRYING_eq_assume_tac (i-1) st;
    8.10  
    8.11  fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
     9.1 --- a/src/HOL/Tools/metis_tools.ML	Mon Jul 06 20:36:38 2009 +0200
     9.2 +++ b/src/HOL/Tools/metis_tools.ML	Mon Jul 06 21:24:30 2009 +0200
     9.3 @@ -339,7 +339,7 @@
     9.4      could then fail. See comment on mk_var.*)
     9.5    fun resolve_inc_tyvars(tha,i,thb) =
     9.6      let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
     9.7 -	val ths = Seq.list_of (bicompose false (false,tha,nprems_of tha) i thb)
     9.8 +	val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
     9.9      in
    9.10  	case distinct Thm.eq_thm ths of
    9.11  	  [th] => th
    10.1 --- a/src/Provers/blast.ML	Mon Jul 06 20:36:38 2009 +0200
    10.2 +++ b/src/Provers/blast.ML	Mon Jul 06 21:24:30 2009 +0200
    10.3 @@ -473,7 +473,7 @@
    10.4  
    10.5  
    10.6  (*Like dup_elim, but puts the duplicated major premise FIRST*)
    10.7 -fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd;
    10.8 +fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
    10.9  
   10.10  
   10.11  (*Rotate the assumptions in all new subgoals for the LIFO discipline*)
   10.12 @@ -485,7 +485,7 @@
   10.13  
   10.14    fun rot_tac [] i st      = Seq.single st
   10.15      | rot_tac (0::ks) i st = rot_tac ks (i+1) st
   10.16 -    | rot_tac (k::ks) i st = rot_tac ks (i+1) (rotate_rule (~k) i st);
   10.17 +    | rot_tac (k::ks) i st = rot_tac ks (i+1) (Thm.rotate_rule (~k) i st);
   10.18  in
   10.19  fun rot_subgoals_tac (rot, rl) =
   10.20       rot_tac (if rot then map nNewHyps rl else [])
    11.1 --- a/src/Provers/classical.ML	Mon Jul 06 20:36:38 2009 +0200
    11.2 +++ b/src/Provers/classical.ML	Mon Jul 06 21:24:30 2009 +0200
    11.3 @@ -209,7 +209,7 @@
    11.4  
    11.5  fun dup_elim th =
    11.6      rule_by_tactic (TRYALL (etac revcut_rl))
    11.7 -      ((th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd);
    11.8 +      ((th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd);
    11.9  
   11.10  (**** Classical rule sets ****)
   11.11  
    12.1 --- a/src/Pure/Isar/rule_insts.ML	Mon Jul 06 20:36:38 2009 +0200
    12.2 +++ b/src/Pure/Isar/rule_insts.ML	Mon Jul 06 21:24:30 2009 +0200
    12.3 @@ -354,7 +354,7 @@
    12.4        instantiate ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
    12.5          (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
    12.6    in
    12.7 -    (case Seq.list_of (bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
    12.8 +    (case Seq.list_of (Thm.bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
    12.9        [th] => th
   12.10      | _ => raise THM ("make_elim_preserve", 1, [rl]))
   12.11    end;
    13.1 --- a/src/Pure/drule.ML	Mon Jul 06 20:36:38 2009 +0200
    13.2 +++ b/src/Pure/drule.ML	Mon Jul 06 21:24:30 2009 +0200
    13.3 @@ -373,23 +373,25 @@
    13.4  
    13.5  (*Rotates a rule's premises to the left by k*)
    13.6  fun rotate_prems 0 = I
    13.7 -  | rotate_prems k = permute_prems 0 k;
    13.8 +  | rotate_prems k = Thm.permute_prems 0 k;
    13.9  
   13.10  fun with_subgoal i f = rotate_prems (i - 1) #> f #> rotate_prems (1 - i);
   13.11  
   13.12 -(* permute prems, where the i-th position in the argument list (counting from 0)
   13.13 -   gives the position within the original thm to be transferred to position i.
   13.14 -   Any remaining trailing positions are left unchanged. *)
   13.15 -val rearrange_prems = let
   13.16 -  fun rearr new []      thm = thm
   13.17 -  |   rearr new (p::ps) thm = rearr (new+1)
   13.18 -     (map (fn q => if new<=q andalso q<p then q+1 else q) ps)
   13.19 -     (permute_prems (new+1) (new-p) (permute_prems new (p-new) thm))
   13.20 +(*Permute prems, where the i-th position in the argument list (counting from 0)
   13.21 +  gives the position within the original thm to be transferred to position i.
   13.22 +  Any remaining trailing positions are left unchanged.*)
   13.23 +val rearrange_prems =
   13.24 +  let
   13.25 +    fun rearr new [] thm = thm
   13.26 +      | rearr new (p :: ps) thm =
   13.27 +          rearr (new + 1)
   13.28 +            (map (fn q => if new <= q andalso q < p then q + 1 else q) ps)
   13.29 +            (Thm.permute_prems (new + 1) (new - p) (Thm.permute_prems new (p - new) thm))
   13.30    in rearr 0 end;
   13.31  
   13.32  (*Resolution: exactly one resolvent must be produced.*)
   13.33  fun tha RSN (i,thb) =
   13.34 -  case Seq.chop 2 (biresolution false [(false,tha)] i thb) of
   13.35 +  case Seq.chop 2 (Thm.biresolution false [(false,tha)] i thb) of
   13.36        ([th],_) => th
   13.37      | ([],_)   => raise THM("RSN: no unifiers", i, [tha,thb])
   13.38      |      _   => raise THM("RSN: multiple unifiers", i, [tha,thb]);
   13.39 @@ -399,7 +401,7 @@
   13.40  
   13.41  (*For joining lists of rules*)
   13.42  fun thas RLN (i,thbs) =
   13.43 -  let val resolve = biresolution false (map (pair false) thas) i
   13.44 +  let val resolve = Thm.biresolution false (map (pair false) thas) i
   13.45        fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
   13.46    in maps resb thbs end;
   13.47  
   13.48 @@ -425,7 +427,7 @@
   13.49    with no lifting or renaming!  Q may contain ==> or meta-quants
   13.50    ALWAYS deletes premise i *)
   13.51  fun compose(tha,i,thb) =
   13.52 -    distinct Thm.eq_thm (Seq.list_of (bicompose false (false,tha,0) i thb));
   13.53 +    distinct Thm.eq_thm (Seq.list_of (Thm.bicompose false (false,tha,0) i thb));
   13.54  
   13.55  fun compose_single (tha,i,thb) =
   13.56    case compose (tha,i,thb) of
    14.1 --- a/src/Pure/tactic.ML	Mon Jul 06 20:36:38 2009 +0200
    14.2 +++ b/src/Pure/tactic.ML	Mon Jul 06 21:24:30 2009 +0200
    14.3 @@ -105,24 +105,24 @@
    14.4       thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
    14.5  
    14.6  (*Solve subgoal i by assumption*)
    14.7 -fun assume_tac i = PRIMSEQ (assumption i);
    14.8 +fun assume_tac i = PRIMSEQ (Thm.assumption i);
    14.9  
   14.10  (*Solve subgoal i by assumption, using no unification*)
   14.11 -fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
   14.12 +fun eq_assume_tac i = PRIMITIVE (Thm.eq_assumption i);
   14.13  
   14.14  
   14.15  (** Resolution/matching tactics **)
   14.16  
   14.17  (*The composition rule/state: no lifting or var renaming.
   14.18 -  The arg = (bires_flg, orule, m) ;  see bicompose for explanation.*)
   14.19 -fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
   14.20 +  The arg = (bires_flg, orule, m);  see Thm.bicompose for explanation.*)
   14.21 +fun compose_tac arg i = PRIMSEQ (Thm.bicompose false arg i);
   14.22  
   14.23  (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   14.24    like [| P&Q; P==>R |] ==> R *)
   14.25  fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
   14.26  
   14.27  (*Attack subgoal i by resolution, using flags to indicate elimination rules*)
   14.28 -fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
   14.29 +fun biresolve_tac brules i = PRIMSEQ (Thm.biresolution false brules i);
   14.30  
   14.31  (*Resolution: the simple case, works for introduction rules*)
   14.32  fun resolve_tac rules = biresolve_tac (map (pair false) rules);
   14.33 @@ -152,7 +152,7 @@
   14.34  fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
   14.35  
   14.36  (*Matching tactics -- as above, but forbid updating of state*)
   14.37 -fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
   14.38 +fun bimatch_tac brules i = PRIMSEQ (Thm.biresolution true brules i);
   14.39  fun match_tac rules  = bimatch_tac (map (pair false) rules);
   14.40  fun ematch_tac rules = bimatch_tac (map (pair true) rules);
   14.41  fun dmatch_tac rls   = ematch_tac (map make_elim rls);
   14.42 @@ -295,7 +295,7 @@
   14.43        let val hyps = Logic.strip_assums_hyp prem
   14.44            and concl = Logic.strip_assums_concl prem
   14.45            val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps
   14.46 -      in PRIMSEQ (biresolution match (order kbrls) i) end);
   14.47 +      in PRIMSEQ (Thm.biresolution match (order kbrls) i) end);
   14.48  
   14.49  (*versions taking pre-built nets.  No filtering of brls*)
   14.50  val biresolve_from_nets_tac = biresolution_from_nets_tac order_list false;
   14.51 @@ -326,7 +326,7 @@
   14.52        in
   14.53           if pred krls
   14.54           then PRIMSEQ
   14.55 -                (biresolution match (map (pair false) (order_list krls)) i)
   14.56 +                (Thm.biresolution match (map (pair false) (order_list krls)) i)
   14.57           else no_tac
   14.58        end);
   14.59  
   14.60 @@ -359,15 +359,15 @@
   14.61  fun rename_tac xs i =
   14.62    case Library.find_first (not o Syntax.is_identifier) xs of
   14.63        SOME x => error ("Not an identifier: " ^ x)
   14.64 -    | NONE => PRIMITIVE (rename_params_rule (xs, i));
   14.65 +    | NONE => PRIMITIVE (Thm.rename_params_rule (xs, i));
   14.66  
   14.67  (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   14.68    right to left if n is positive, and from left to right if n is negative.*)
   14.69  fun rotate_tac 0 i = all_tac
   14.70 -  | rotate_tac k i = PRIMITIVE (rotate_rule k i);
   14.71 +  | rotate_tac k i = PRIMITIVE (Thm.rotate_rule k i);
   14.72  
   14.73  (*Rotates the given subgoal to be the last.*)
   14.74 -fun defer_tac i = PRIMITIVE (permute_prems (i-1) 1);
   14.75 +fun defer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1);
   14.76  
   14.77  (* remove premises that do not satisfy p; fails if all prems satisfy p *)
   14.78  fun filter_prems_tac p =
    15.1 --- a/src/Pure/tctical.ML	Mon Jul 06 20:36:38 2009 +0200
    15.2 +++ b/src/Pure/tctical.ML	Mon Jul 06 21:24:30 2009 +0200
    15.3 @@ -463,8 +463,7 @@
    15.4                    (forall_intr_list cparams (implies_intr_list chyps Cth)))
    15.5          end
    15.6        (*function to replace the current subgoal*)
    15.7 -      fun next st = bicompose false (false, relift st, nprems_of st)
    15.8 -                    gno state
    15.9 +      fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
   15.10    in Seq.maps next (tacf subprems (trivial (cterm concl))) end;
   15.11  
   15.12  end;
    16.1 --- a/src/Pure/thm.ML	Mon Jul 06 20:36:38 2009 +0200
    16.2 +++ b/src/Pure/thm.ML	Mon Jul 06 21:24:30 2009 +0200
    16.3 @@ -97,14 +97,6 @@
    16.4    val dest_state: thm * int -> (term * term) list * term list * term * term
    16.5    val lift_rule: cterm -> thm -> thm
    16.6    val incr_indexes: int -> thm -> thm
    16.7 -  val assumption: int -> thm -> thm Seq.seq
    16.8 -  val eq_assumption: int -> thm -> thm
    16.9 -  val rotate_rule: int -> int -> thm -> thm
   16.10 -  val permute_prems: int -> int -> thm -> thm
   16.11 -  val rename_params_rule: string list * int -> thm -> thm
   16.12 -  val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
   16.13 -  val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
   16.14 -  val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   16.15  end;
   16.16  
   16.17  signature THM =
   16.18 @@ -117,37 +109,45 @@
   16.19    val dest_fun2: cterm -> cterm
   16.20    val dest_arg1: cterm -> cterm
   16.21    val dest_abs: string option -> cterm -> cterm * cterm
   16.22 -  val adjust_maxidx_cterm: int -> cterm -> cterm
   16.23    val capply: cterm -> cterm -> cterm
   16.24    val cabs: cterm -> cterm -> cterm
   16.25 -  val major_prem_of: thm -> term
   16.26 -  val no_prems: thm -> bool
   16.27 +  val adjust_maxidx_cterm: int -> cterm -> cterm
   16.28 +  val incr_indexes_cterm: int -> cterm -> cterm
   16.29 +  val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
   16.30 +  val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
   16.31    val terms_of_tpairs: (term * term) list -> term list
   16.32 +  val full_prop_of: thm -> term
   16.33    val maxidx_of: thm -> int
   16.34    val maxidx_thm: thm -> int -> int
   16.35    val hyps_of: thm -> term list
   16.36 -  val full_prop_of: thm -> term
   16.37 +  val no_prems: thm -> bool
   16.38 +  val major_prem_of: thm -> term
   16.39    val axiom: theory -> string -> thm
   16.40    val axioms_of: theory -> (string * thm) list
   16.41 -  val get_name: thm -> string
   16.42 -  val put_name: string -> thm -> thm
   16.43    val get_tags: thm -> Properties.T
   16.44    val map_tags: (Properties.T -> Properties.T) -> thm -> thm
   16.45    val norm_proof: thm -> thm
   16.46    val adjust_maxidx_thm: int -> thm -> thm
   16.47 -  val rename_boundvars: term -> term -> thm -> thm
   16.48 -  val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
   16.49 -  val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
   16.50 -  val incr_indexes_cterm: int -> cterm -> cterm
   16.51    val varifyT: thm -> thm
   16.52    val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   16.53    val freezeT: thm -> thm
   16.54 +  val assumption: int -> thm -> thm Seq.seq
   16.55 +  val eq_assumption: int -> thm -> thm
   16.56 +  val rotate_rule: int -> int -> thm -> thm
   16.57 +  val permute_prems: int -> int -> thm -> thm
   16.58 +  val rename_params_rule: string list * int -> thm -> thm
   16.59 +  val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
   16.60 +  val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
   16.61 +  val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   16.62 +  val rename_boundvars: term -> term -> thm -> thm
   16.63    val future: thm future -> cterm -> thm
   16.64    val pending_groups: thm -> Task_Queue.group list -> Task_Queue.group list
   16.65    val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
   16.66    val proof_body_of: thm -> proof_body
   16.67    val proof_of: thm -> proof
   16.68    val join_proof: thm -> unit
   16.69 +  val get_name: thm -> string
   16.70 +  val put_name: string -> thm -> thm
   16.71    val extern_oracles: theory -> xstring list
   16.72    val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
   16.73  end;
    17.1 --- a/src/Tools/IsaPlanner/isand.ML	Mon Jul 06 20:36:38 2009 +0200
    17.2 +++ b/src/Tools/IsaPlanner/isand.ML	Mon Jul 06 21:24:30 2009 +0200
    17.3 @@ -110,7 +110,7 @@
    17.4  fun solve_with sol th = 
    17.5      let fun solvei 0 = Seq.empty
    17.6            | solvei i = 
    17.7 -            Seq.append (bicompose false (false,sol,0) i th) (solvei (i - 1))
    17.8 +            Seq.append (Thm.bicompose false (false,sol,0) i th) (solvei (i - 1))
    17.9      in
   17.10        solvei (Thm.nprems_of th)
   17.11      end;
   17.12 @@ -337,7 +337,7 @@
   17.13  
   17.14        val newth' = Drule.implies_intr_list sgallcts allified_newth
   17.15      in
   17.16 -      bicompose false (false, newth', (length sgallcts)) i gth
   17.17 +      Thm.bicompose false (false, newth', (length sgallcts)) i gth
   17.18      end;
   17.19  
   17.20  (*