--- a/src/HOL/Bali/AxCompl.thy Mon Jul 06 16:49:51 2009 +0200
+++ b/src/HOL/Bali/AxCompl.thy Tue Jul 07 07:56:24 2009 +0200
@@ -1402,7 +1402,7 @@
apply -
apply (induct_tac "n")
apply (tactic "ALLGOALS (clarsimp_tac @{clasimpset})")
-apply (tactic {* dtac (permute_prems 0 1 (thm "card_seteq")) 1 *})
+apply (tactic {* dtac (Thm.permute_prems 0 1 (thm "card_seteq")) 1 *})
apply simp
apply (erule finite_imageI)
apply (simp add: MGF_asm ax_derivs_asm)
--- a/src/HOL/Import/import.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/HOL/Import/import.ML Tue Jul 07 07:56:24 2009 +0200
@@ -55,7 +55,7 @@
then message "import: Terms match up"
else message "import: Terms DO NOT match up"
val thm' = equal_elim (symmetric prew) thm
- val res = bicompose true (false,thm',0) 1 th
+ val res = Thm.bicompose true (false,thm',0) 1 th
in
res
end
--- a/src/HOL/Import/proof_kernel.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Tue Jul 07 07:56:24 2009 +0200
@@ -977,7 +977,7 @@
fun uniq_compose m th i st =
let
- val res = bicompose false (false,th,m) i st
+ val res = Thm.bicompose false (false,th,m) i st
in
case Seq.pull res of
SOME (th,rest) => (case Seq.pull rest of
@@ -1065,14 +1065,12 @@
res
end
-val permute_prems = Thm.permute_prems
-
fun rearrange sg tm th =
let
val tm' = Envir.beta_eta_contract tm
- fun find [] n = permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
+ fun find [] n = Thm.permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
| find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p)
- then permute_prems n 1 th
+ then Thm.permute_prems n 1 th
else find ps (n+1)
in
find (prems_of th) 0
@@ -1193,7 +1191,7 @@
fun if_debug f x = if !debug then f x else ()
val message = if_debug writeln
-val conjE_helper = permute_prems 0 1 conjE
+val conjE_helper = Thm.permute_prems 0 1 conjE
fun get_hol4_thm thyname thmname thy =
case get_hol4_theorem thyname thmname thy of
--- a/src/HOL/Import/shuffler.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/HOL/Import/shuffler.ML Tue Jul 07 07:56:24 2009 +0200
@@ -595,7 +595,7 @@
val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
val triv_th = trivial rhs
val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
- val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
+ val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
SOME(th,_) => SOME th
| NONE => NONE
in
--- a/src/HOL/Set.thy Mon Jul 06 16:49:51 2009 +0200
+++ b/src/HOL/Set.thy Tue Jul 07 07:56:24 2009 +0200
@@ -449,7 +449,7 @@
lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
by (unfold Ball_def) blast
-ML {* bind_thm ("rev_ballE", permute_prems 1 1 @{thm ballE}) *}
+ML {* bind_thm ("rev_ballE", Thm.permute_prems 1 1 @{thm ballE}) *}
text {*
\medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and
--- a/src/HOL/TLA/Intensional.thy Mon Jul 06 16:49:51 2009 +0200
+++ b/src/HOL/TLA/Intensional.thy Tue Jul 07 07:56:24 2009 +0200
@@ -268,7 +268,7 @@
let
(* analogous to RS, but using matching instead of resolution *)
fun matchres tha i thb =
- case Seq.chop 2 (biresolution true [(false,tha)] i thb) of
+ case Seq.chop 2 (Thm.biresolution true [(false,tha)] i thb) of
([th],_) => th
| ([],_) => raise THM("matchres: no match", i, [tha,thb])
| _ => raise THM("matchres: multiple unifiers", i, [tha,thb])
--- a/src/HOL/Tools/TFL/rules.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Tue Jul 07 07:56:24 2009 +0200
@@ -519,14 +519,14 @@
handle TERM _ => get (rst, n+1, L)
| U.ERR _ => get (rst, n+1, L);
-(* Note: rename_params_rule counts from 1, not 0 *)
+(* Note: Thm.rename_params_rule counts from 1, not 0 *)
fun rename thm =
let val thy = Thm.theory_of_thm thm
val tych = cterm_of thy
val ants = Logic.strip_imp_prems (Thm.prop_of thm)
val news = get (ants,1,[])
in
- fold rename_params_rule news thm
+ fold Thm.rename_params_rule news thm
end;
--- a/src/HOL/Tools/meson.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/HOL/Tools/meson.ML Tue Jul 07 07:56:24 2009 +0200
@@ -470,7 +470,7 @@
(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
fun TRYING_eq_assume_tac 0 st = Seq.single st
| TRYING_eq_assume_tac i st =
- TRYING_eq_assume_tac (i-1) (eq_assumption i st)
+ TRYING_eq_assume_tac (i-1) (Thm.eq_assumption i st)
handle THM _ => TRYING_eq_assume_tac (i-1) st;
fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
--- a/src/HOL/Tools/metis_tools.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Tue Jul 07 07:56:24 2009 +0200
@@ -339,7 +339,7 @@
could then fail. See comment on mk_var.*)
fun resolve_inc_tyvars(tha,i,thb) =
let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
- val ths = Seq.list_of (bicompose false (false,tha,nprems_of tha) i thb)
+ val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
in
case distinct Thm.eq_thm ths of
[th] => th
--- a/src/HOL/Tools/refute.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/HOL/Tools/refute.ML Tue Jul 07 07:56:24 2009 +0200
@@ -909,8 +909,8 @@
(* and the class definition *)
let
val class = Logic.class_of_const s
- val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class)
- val ax_in = SOME (specialize_type thy (s, T) inclass)
+ val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), class)
+ val ax_in = SOME (specialize_type thy (s, T) of_class)
(* type match may fail due to sort constraints *)
handle Type.TYPE_MATCH => NONE
val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax))
--- a/src/Provers/blast.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Provers/blast.ML Tue Jul 07 07:56:24 2009 +0200
@@ -473,7 +473,7 @@
(*Like dup_elim, but puts the duplicated major premise FIRST*)
-fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd;
+fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
(*Rotate the assumptions in all new subgoals for the LIFO discipline*)
@@ -485,7 +485,7 @@
fun rot_tac [] i st = Seq.single st
| rot_tac (0::ks) i st = rot_tac ks (i+1) st
- | rot_tac (k::ks) i st = rot_tac ks (i+1) (rotate_rule (~k) i st);
+ | rot_tac (k::ks) i st = rot_tac ks (i+1) (Thm.rotate_rule (~k) i st);
in
fun rot_subgoals_tac (rot, rl) =
rot_tac (if rot then map nNewHyps rl else [])
--- a/src/Provers/classical.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Provers/classical.ML Tue Jul 07 07:56:24 2009 +0200
@@ -209,7 +209,7 @@
fun dup_elim th =
rule_by_tactic (TRYALL (etac revcut_rl))
- ((th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd);
+ ((th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd);
(**** Classical rule sets ****)
--- a/src/Pure/Isar/class.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Pure/Isar/class.ML Tue Jul 07 07:56:24 2009 +0200
@@ -83,14 +83,14 @@
(fst (Locale.intros_of thy class));
(* of_class *)
- val of_class_prop_concl = Logic.mk_inclass (aT, class);
+ val of_class_prop_concl = Logic.mk_of_class (aT, class);
val of_class_prop = case prop of NONE => of_class_prop_concl
| SOME prop => Logic.mk_implies (Morphism.term const_morph
((map_types o map_atyps) (K aT) prop), of_class_prop_concl);
val sup_of_classes = map (snd o rules thy) sups;
val loc_axiom_intros = map Drule.standard' (Locale.axioms_of thy class);
val axclass_intro = #intro (AxClass.get_info thy class);
- val base_sort_trivs = Thm.sort_triv thy (aT, base_sort);
+ val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
val tac = REPEAT (SOMEGOAL
(Tactic.match_tac (axclass_intro :: sup_of_classes
@ loc_axiom_intros @ base_sort_trivs)
--- a/src/Pure/Isar/rule_insts.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Pure/Isar/rule_insts.ML Tue Jul 07 07:56:24 2009 +0200
@@ -354,7 +354,7 @@
instantiate ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
(cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
in
- (case Seq.list_of (bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
+ (case Seq.list_of (Thm.bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
[th] => th
| _ => raise THM ("make_elim_preserve", 1, [rl]))
end;
--- a/src/Pure/Proof/proof_syntax.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Tue Jul 07 07:56:24 2009 +0200
@@ -54,7 +54,7 @@
(Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn),
(Binding.name "Hyp", propT --> proofT, NoSyn),
(Binding.name "Oracle", propT --> proofT, NoSyn),
- (Binding.name "Inclass", (Term.a_itselfT --> propT) --> proofT, NoSyn),
+ (Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT, NoSyn),
(Binding.name "MinProof", proofT, Delimfix "?")]
|> Sign.add_nonterminals [Binding.name "param", Binding.name "params"]
|> Sign.add_syntax_i
@@ -113,11 +113,11 @@
| NONE => error ("Unknown theorem " ^ quote name))
end
| _ => error ("Illegal proof constant name: " ^ quote s))
- | prf_of Ts (Const ("Inclass", _) $ Const (c_class, _)) =
+ | prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) =
(case try Logic.class_of_const c_class of
SOME c =>
change_type (if ty then SOME Ts else NONE)
- (Inclass (TVar ((Name.aT, 0), []), c))
+ (OfClass (TVar ((Name.aT, 0), []), c))
| NONE => error ("Bad class constant: " ^ quote c_class))
| prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop
| prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v
@@ -148,7 +148,7 @@
val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);
val Hypt = Const ("Hyp", propT --> proofT);
val Oraclet = Const ("Oracle", propT --> proofT);
-val Inclasst = Const ("Inclass", (Term.itselfT dummyT --> propT) --> proofT);
+val OfClasst = Const ("OfClass", (Term.itselfT dummyT --> propT) --> proofT);
val MinProoft = Const ("MinProof", proofT);
val mk_tyapp = fold (fn T => fn prf => Const ("Appt",
@@ -161,8 +161,8 @@
| term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT)
| term_of _ (PAxm (name, _, SOME Ts)) =
mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT))
- | term_of _ (Inclass (T, c)) =
- mk_tyapp [T] (Inclasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT))
+ | term_of _ (OfClass (T, c)) =
+ mk_tyapp [T] (OfClasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT))
| term_of _ (PBound i) = Bound i
| term_of Ts (Abst (s, opT, prf)) =
let val T = the_default dummyT opT
--- a/src/Pure/Proof/reconstruct.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML Tue Jul 07 07:56:24 2009 +0200
@@ -223,8 +223,8 @@
mk_cnstrts_atom env vTs prop opTs prf
| mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) =
mk_cnstrts_atom env vTs prop opTs prf
- | mk_cnstrts env _ _ vTs (prf as Inclass (T, c)) =
- mk_cnstrts_atom env vTs (Logic.mk_inclass (T, c)) NONE prf
+ | mk_cnstrts env _ _ vTs (prf as OfClass (T, c)) =
+ mk_cnstrts_atom env vTs (Logic.mk_of_class (T, c)) NONE prf
| mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) =
mk_cnstrts_atom env vTs prop opTs prf
| mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs)
@@ -321,7 +321,7 @@
| prop_of0 Hs (Hyp t) = t
| prop_of0 Hs (PThm (_, ((_, prop, SOME Ts), _))) = prop_of_atom prop Ts
| prop_of0 Hs (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts
- | prop_of0 Hs (Inclass (T, c)) = Logic.mk_inclass (T, c)
+ | prop_of0 Hs (OfClass (T, c)) = Logic.mk_of_class (T, c)
| prop_of0 Hs (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
| prop_of0 _ _ = error "prop_of: partial proof object";
--- a/src/Pure/axclass.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Pure/axclass.ML Tue Jul 07 07:56:24 2009 +0200
@@ -214,7 +214,7 @@
|> snd))
end;
-fun complete_arities thy =
+fun complete_arities thy =
let
val arities = snd (get_instances thy);
val (completions, arities') = arities
@@ -338,10 +338,11 @@
(* primitive rules *)
-fun add_classrel th thy =
+fun add_classrel raw_th thy =
let
+ val th = Thm.strip_shyps (Thm.transfer thy raw_th);
+ val prop = Thm.plain_prop_of th;
fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
- val prop = Thm.plain_prop_of (Thm.transfer thy th);
val rel = Logic.dest_classrel prop handle TERM _ => err ();
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
in
@@ -351,10 +352,11 @@
|> perhaps complete_arities
end;
-fun add_arity th thy =
+fun add_arity raw_th thy =
let
+ val th = Thm.strip_shyps (Thm.transfer thy raw_th);
+ val prop = Thm.plain_prop_of th;
fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
- val prop = Thm.plain_prop_of (Thm.transfer thy th);
val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
val T = Type (t, map TFree (Name.names Name.context Name.aT Ss));
val missing_params = Sign.complete_sort thy [c]
@@ -470,9 +472,9 @@
(* definition *)
- val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ flat axiomss;
+ val conjs = map (curry Logic.mk_of_class (Term.aT [])) super @ flat axiomss;
val class_eq =
- Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_balanced conjs);
+ Logic.mk_equals (Logic.mk_of_class (Term.aT [], class), Logic.mk_conjunction_balanced conjs);
val ([def], def_thy) =
thy
@@ -575,12 +577,13 @@
fun derive_type _ (_, []) = []
| derive_type thy (typ, sort) =
let
+ val certT = Thm.ctyp_of thy;
val vars = Term.fold_atyps
(fn T as TFree (_, S) => insert (eq_fst op =) (T, S)
| T as TVar (_, S) => insert (eq_fst op =) (T, S)
| _ => I) typ [];
val hyps = vars
- |> map (fn (T, S) => (T, Thm.sort_triv thy (T, S) ~~ S));
+ |> map (fn (T, S) => (T, Thm.of_sort (certT T, S) ~~ S));
val ths = (typ, sort)
|> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
{class_relation =
@@ -605,7 +608,7 @@
val ths =
sort |> map (fn c =>
Goal.finish (the (lookup_type cache' typ c) RS
- Goal.init (Thm.cterm_of thy (Logic.mk_inclass (typ, c))))
+ Goal.init (Thm.cterm_of thy (Logic.mk_of_class (typ, c))))
|> Thm.adjust_maxidx_thm ~1);
in (ths, cache') end;
--- a/src/Pure/drule.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Pure/drule.ML Tue Jul 07 07:56:24 2009 +0200
@@ -373,23 +373,25 @@
(*Rotates a rule's premises to the left by k*)
fun rotate_prems 0 = I
- | rotate_prems k = permute_prems 0 k;
+ | rotate_prems k = Thm.permute_prems 0 k;
fun with_subgoal i f = rotate_prems (i - 1) #> f #> rotate_prems (1 - i);
-(* permute prems, where the i-th position in the argument list (counting from 0)
- gives the position within the original thm to be transferred to position i.
- Any remaining trailing positions are left unchanged. *)
-val rearrange_prems = let
- fun rearr new [] thm = thm
- | rearr new (p::ps) thm = rearr (new+1)
- (map (fn q => if new<=q andalso q<p then q+1 else q) ps)
- (permute_prems (new+1) (new-p) (permute_prems new (p-new) thm))
+(*Permute prems, where the i-th position in the argument list (counting from 0)
+ gives the position within the original thm to be transferred to position i.
+ Any remaining trailing positions are left unchanged.*)
+val rearrange_prems =
+ let
+ fun rearr new [] thm = thm
+ | rearr new (p :: ps) thm =
+ rearr (new + 1)
+ (map (fn q => if new <= q andalso q < p then q + 1 else q) ps)
+ (Thm.permute_prems (new + 1) (new - p) (Thm.permute_prems new (p - new) thm))
in rearr 0 end;
(*Resolution: exactly one resolvent must be produced.*)
fun tha RSN (i,thb) =
- case Seq.chop 2 (biresolution false [(false,tha)] i thb) of
+ case Seq.chop 2 (Thm.biresolution false [(false,tha)] i thb) of
([th],_) => th
| ([],_) => raise THM("RSN: no unifiers", i, [tha,thb])
| _ => raise THM("RSN: multiple unifiers", i, [tha,thb]);
@@ -399,7 +401,7 @@
(*For joining lists of rules*)
fun thas RLN (i,thbs) =
- let val resolve = biresolution false (map (pair false) thas) i
+ let val resolve = Thm.biresolution false (map (pair false) thas) i
fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
in maps resb thbs end;
@@ -425,7 +427,7 @@
with no lifting or renaming! Q may contain ==> or meta-quants
ALWAYS deletes premise i *)
fun compose(tha,i,thb) =
- distinct Thm.eq_thm (Seq.list_of (bicompose false (false,tha,0) i thb));
+ distinct Thm.eq_thm (Seq.list_of (Thm.bicompose false (false,tha,0) i thb));
fun compose_single (tha,i,thb) =
case compose (tha,i,thb) of
--- a/src/Pure/logic.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Pure/logic.ML Tue Jul 07 07:56:24 2009 +0200
@@ -36,8 +36,8 @@
val type_map: (term -> term) -> typ -> typ
val const_of_class: class -> string
val class_of_const: string -> class
- val mk_inclass: typ * class -> term
- val dest_inclass: term -> typ * class
+ val mk_of_class: typ * class -> term
+ val dest_of_class: term -> typ * class
val name_classrel: string * string -> string
val mk_classrel: class * class -> term
val dest_classrel: term -> class * class
@@ -219,13 +219,13 @@
handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
-(* class constraints *)
+(* class membership *)
-fun mk_inclass (ty, c) =
+fun mk_of_class (ty, c) =
Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
-fun dest_inclass (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
- | dest_inclass t = raise TERM ("dest_inclass", [t]);
+fun dest_of_class (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
+ | dest_of_class t = raise TERM ("dest_of_class", [t]);
(* class relations *)
@@ -233,10 +233,10 @@
fun name_classrel (c1, c2) =
Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2;
-fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2);
+fun mk_classrel (c1, c2) = mk_of_class (Term.aT [c1], c2);
fun dest_classrel tm =
- (case dest_inclass tm of
+ (case dest_of_class tm of
(TVar (_, [c1]), c2) => (c1, c2)
| _ => raise TERM ("dest_classrel", [tm]));
@@ -251,13 +251,13 @@
fun mk_arities (t, Ss, S) =
let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
- in map (fn c => mk_inclass (T, c)) S end;
+ in map (fn c => mk_of_class (T, c)) S end;
fun dest_arity tm =
let
fun err () = raise TERM ("dest_arity", [tm]);
- val (ty, c) = dest_inclass tm;
+ val (ty, c) = dest_of_class tm;
val (t, tvars) =
(case ty of
Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ())
--- a/src/Pure/more_thm.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Pure/more_thm.ML Tue Jul 07 07:56:24 2009 +0200
@@ -26,11 +26,11 @@
val eq_thm_thy: thm * thm -> bool
val eq_thm_prop: thm * thm -> bool
val equiv_thm: thm * thm -> bool
- val sort_triv: theory -> typ * sort -> thm list
+ val class_triv: theory -> class -> thm
+ val of_sort: ctyp * sort -> thm list
val check_shyps: sort list -> thm -> thm
val is_dummy: thm -> bool
val plain_prop_of: thm -> term
- val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
val add_thm: thm -> thm list -> thm list
val del_thm: thm -> thm list -> thm list
val merge_thms: thm list * thm list -> thm list
@@ -171,14 +171,10 @@
(* type classes and sorts *)
-fun sort_triv thy (T, S) =
- let
- val certT = Thm.ctyp_of thy;
- val cT = certT T;
- fun class_triv c =
- Thm.class_triv thy c
- |> Thm.instantiate ([(certT (TVar ((Name.aT, 0), [c])), cT)], []);
- in map class_triv S end;
+fun class_triv thy c =
+ Thm.of_class (Thm.ctyp_of thy (TVar ((Name.aT, 0), [c])), c);
+
+fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S;
fun check_shyps sorts raw_th =
let
@@ -214,10 +210,6 @@
else prop
end;
-fun fold_terms f th =
- let val {tpairs, prop, hyps, ...} = Thm.rep_thm th
- in fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps end;
-
(* collections of theorems in canonical order *)
--- a/src/Pure/proofterm.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Pure/proofterm.ML Tue Jul 07 07:56:24 2009 +0200
@@ -19,7 +19,7 @@
| op %% of proof * proof
| Hyp of term
| PAxm of string * term * typ list option
- | Inclass of typ * class
+ | OfClass of typ * class
| Oracle of string * term * typ list option
| Promise of serial * term * typ list
| PThm of serial * ((string * term * typ list option) * proof_body future)
@@ -141,7 +141,7 @@
| op %% of proof * proof
| Hyp of term
| PAxm of string * term * typ list option
- | Inclass of typ * class
+ | OfClass of typ * class
| Oracle of string * term * typ list option
| Promise of serial * term * typ list
| PThm of serial * ((string * term * typ list option) * proof_body future)
@@ -292,7 +292,7 @@
| mapp (prf1 %% prf2) = (mapp prf1 %% mapph prf2
handle SAME => prf1 %% mapp prf2)
| mapp (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (map_typs Ts))
- | mapp (Inclass (T, c)) = Inclass (apsome g (SOME T) |> the, c)
+ | mapp (OfClass (T, c)) = OfClass (apsome g (SOME T) |> the, c)
| mapp (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (map_typs Ts))
| mapp (Promise (i, prop, Ts)) = Promise (i, prop, map_typs Ts)
| mapp (PThm (i, ((a, prop, SOME Ts), body))) =
@@ -320,7 +320,7 @@
| fold_proof_terms f g (prf1 %% prf2) =
fold_proof_terms f g prf1 #> fold_proof_terms f g prf2
| fold_proof_terms _ g (PAxm (_, _, SOME Ts)) = fold g Ts
- | fold_proof_terms _ g (Inclass (T, _)) = g T
+ | fold_proof_terms _ g (OfClass (T, _)) = g T
| fold_proof_terms _ g (Oracle (_, _, SOME Ts)) = fold g Ts
| fold_proof_terms _ g (Promise (_, _, Ts)) = fold g Ts
| fold_proof_terms _ g (PThm (_, ((_, _, SOME Ts), _))) = fold g Ts
@@ -335,7 +335,7 @@
| size_of_proof _ = 1;
fun change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs)
- | change_type (SOME [T]) (Inclass (_, c)) = Inclass (T, c)
+ | change_type (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
| change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)
| change_type opTs (Promise _) = error "change_type: unexpected promise"
| change_type opTs (PThm (i, ((name, prop, _), body))) = PThm (i, ((name, prop, opTs), body))
@@ -473,7 +473,7 @@
| norm (prf1 %% prf2) = (norm prf1 %% normh prf2
handle SAME => prf1 %% norm prf2)
| norm (PAxm (s, prop, Ts)) = PAxm (s, prop, apsome' (htypeTs norm_types_same) Ts)
- | norm (Inclass (T, c)) = Inclass (htypeT norm_type_same T, c)
+ | norm (OfClass (T, c)) = OfClass (htypeT norm_type_same T, c)
| norm (Oracle (s, prop, Ts)) = Oracle (s, prop, apsome' (htypeTs norm_types_same) Ts)
| norm (Promise (i, prop, Ts)) = Promise (i, prop, htypeTs norm_types_same Ts)
| norm (PThm (i, ((s, t, Ts), body))) =
@@ -719,8 +719,8 @@
handle SAME => prf1 %% lift' Us Ts prf2)
| lift' _ _ (PAxm (s, prop, Ts)) =
PAxm (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts)
- | lift' _ _ (Inclass (T, c)) =
- Inclass (same (op =) (Logic.incr_tvar inc) T, c)
+ | lift' _ _ (OfClass (T, c)) =
+ OfClass (same (op =) (Logic.incr_tvar inc) T, c)
| lift' _ _ (Oracle (s, prop, Ts)) =
Oracle (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts)
| lift' _ _ (Promise (i, prop, Ts)) =
@@ -977,7 +977,7 @@
orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
| shrink' ls lev ts prfs (prf as Hyp _) = ([], false, map (pair false) ts, prf)
| shrink' ls lev ts prfs (prf as MinProof) = ([], false, map (pair false) ts, prf)
- | shrink' ls lev ts prfs (prf as Inclass _) = ([], false, map (pair false) ts, prf)
+ | shrink' ls lev ts prfs (prf as OfClass _) = ([], false, map (pair false) ts, prf)
| shrink' ls lev ts prfs prf =
let
val prop =
@@ -1069,7 +1069,7 @@
| mtch Ts i j inst (PAxm (s1, _, opTs), PAxm (s2, _, opUs)) =
if s1 = s2 then optmatch matchTs inst (opTs, opUs)
else raise PMatch
- | mtch Ts i j inst (Inclass (T1, c1), Inclass (T2, c2)) =
+ | mtch Ts i j inst (OfClass (T1, c1), OfClass (T2, c2)) =
if c1 = c2 then matchT inst (T1, T2)
else raise PMatch
| mtch Ts i j inst (PThm (_, ((name1, prop1, opTs), _)), PThm (_, ((name2, prop2, opUs), _))) =
@@ -1103,7 +1103,7 @@
NONE => prf
| SOME prf' => incr_pboundvars plev tlev prf')
| subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Option.map (map substT) Ts)
- | subst _ _ (Inclass (T, c)) = Inclass (substT T, c)
+ | subst _ _ (OfClass (T, c)) = OfClass (substT T, c)
| subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Option.map (map substT) Ts)
| subst _ _ (Promise (i, prop, Ts)) = Promise (i, prop, (map substT) Ts)
| subst _ _ (PThm (i, ((id, prop, Ts), body))) =
@@ -1130,7 +1130,7 @@
(_, Hyp (Var _)) => true
| (Hyp (Var _), _) => true
| (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2
- | (Inclass (_, c), Inclass (_, d)) => c = d andalso matchrands prf1 prf2
+ | (OfClass (_, c), OfClass (_, d)) => c = d andalso matchrands prf1 prf2
| (PThm (_, ((a, propa, _), _)), PThm (_, ((b, propb, _), _))) =>
a = b andalso propa = propb andalso matchrands prf1 prf2
| (PBound i, PBound j) => i = j andalso matchrands prf1 prf2
--- a/src/Pure/sign.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Pure/sign.ML Tue Jul 07 07:56:24 2009 +0200
@@ -27,7 +27,7 @@
val defaultS: theory -> sort
val subsort: theory -> sort * sort -> bool
val of_sort: theory -> typ * sort -> bool
- val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list
+ val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list
val is_logtype: theory -> string -> bool
val typ_instance: theory -> typ * typ -> bool
val typ_equiv: theory -> typ * typ -> bool
--- a/src/Pure/sorts.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Pure/sorts.ML Tue Jul 07 07:56:24 2009 +0200
@@ -62,7 +62,7 @@
type_constructor: string -> ('a * class) list list -> class -> 'a,
type_variable: typ -> ('a * class) list} ->
typ * sort -> 'a list (*exception CLASS_ERROR*)
- val witness_sorts: algebra -> string list -> sort list -> sort list -> (typ * sort) list
+ val witness_sorts: algebra -> string list -> (typ * sort) list -> sort list -> (typ * sort) list
end;
structure Sorts: SORTS =
@@ -432,18 +432,17 @@
fun witness_sorts algebra types hyps sorts =
let
fun le S1 S2 = sort_le algebra (S1, S2);
- fun get_solved S2 (T, S1) = if le S1 S2 then SOME (T, S2) else NONE;
- fun get_hyp S2 S1 = if le S1 S2 then SOME (TFree ("'hyp", S1), S2) else NONE;
+ fun get S2 (T, S1) = if le S1 S2 then SOME (T, S2) else NONE;
fun mg_dom t S = SOME (mg_domain algebra t S) handle CLASS_ERROR _ => NONE;
fun witn_sort _ [] solved_failed = (SOME (propT, []), solved_failed)
| witn_sort path S (solved, failed) =
if exists (le S) failed then (NONE, (solved, failed))
else
- (case get_first (get_solved S) solved of
+ (case get_first (get S) solved of
SOME w => (SOME w, (solved, failed))
| NONE =>
- (case get_first (get_hyp S) hyps of
+ (case get_first (get S) hyps of
SOME w => (SOME w, (w :: solved, failed))
| NONE => witn_types path types S (solved, failed)))
--- a/src/Pure/tactic.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Pure/tactic.ML Tue Jul 07 07:56:24 2009 +0200
@@ -105,24 +105,24 @@
thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
(*Solve subgoal i by assumption*)
-fun assume_tac i = PRIMSEQ (assumption i);
+fun assume_tac i = PRIMSEQ (Thm.assumption i);
(*Solve subgoal i by assumption, using no unification*)
-fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
+fun eq_assume_tac i = PRIMITIVE (Thm.eq_assumption i);
(** Resolution/matching tactics **)
(*The composition rule/state: no lifting or var renaming.
- The arg = (bires_flg, orule, m) ; see bicompose for explanation.*)
-fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
+ The arg = (bires_flg, orule, m); see Thm.bicompose for explanation.*)
+fun compose_tac arg i = PRIMSEQ (Thm.bicompose false arg i);
(*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
like [| P&Q; P==>R |] ==> R *)
fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
(*Attack subgoal i by resolution, using flags to indicate elimination rules*)
-fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
+fun biresolve_tac brules i = PRIMSEQ (Thm.biresolution false brules i);
(*Resolution: the simple case, works for introduction rules*)
fun resolve_tac rules = biresolve_tac (map (pair false) rules);
@@ -152,7 +152,7 @@
fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
(*Matching tactics -- as above, but forbid updating of state*)
-fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
+fun bimatch_tac brules i = PRIMSEQ (Thm.biresolution true brules i);
fun match_tac rules = bimatch_tac (map (pair false) rules);
fun ematch_tac rules = bimatch_tac (map (pair true) rules);
fun dmatch_tac rls = ematch_tac (map make_elim rls);
@@ -295,7 +295,7 @@
let val hyps = Logic.strip_assums_hyp prem
and concl = Logic.strip_assums_concl prem
val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps
- in PRIMSEQ (biresolution match (order kbrls) i) end);
+ in PRIMSEQ (Thm.biresolution match (order kbrls) i) end);
(*versions taking pre-built nets. No filtering of brls*)
val biresolve_from_nets_tac = biresolution_from_nets_tac order_list false;
@@ -326,7 +326,7 @@
in
if pred krls
then PRIMSEQ
- (biresolution match (map (pair false) (order_list krls)) i)
+ (Thm.biresolution match (map (pair false) (order_list krls)) i)
else no_tac
end);
@@ -359,15 +359,15 @@
fun rename_tac xs i =
case Library.find_first (not o Syntax.is_identifier) xs of
SOME x => error ("Not an identifier: " ^ x)
- | NONE => PRIMITIVE (rename_params_rule (xs, i));
+ | NONE => PRIMITIVE (Thm.rename_params_rule (xs, i));
(*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
right to left if n is positive, and from left to right if n is negative.*)
fun rotate_tac 0 i = all_tac
- | rotate_tac k i = PRIMITIVE (rotate_rule k i);
+ | rotate_tac k i = PRIMITIVE (Thm.rotate_rule k i);
(*Rotates the given subgoal to be the last.*)
-fun defer_tac i = PRIMITIVE (permute_prems (i-1) 1);
+fun defer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1);
(* remove premises that do not satisfy p; fails if all prems satisfy p *)
fun filter_prems_tac p =
--- a/src/Pure/tctical.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Pure/tctical.ML Tue Jul 07 07:56:24 2009 +0200
@@ -463,8 +463,7 @@
(forall_intr_list cparams (implies_intr_list chyps Cth)))
end
(*function to replace the current subgoal*)
- fun next st = bicompose false (false, relift st, nprems_of st)
- gno state
+ fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
in Seq.maps next (tacf subprems (trivial (cterm concl))) end;
end;
--- a/src/Pure/thm.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Pure/thm.ML Tue Jul 07 07:56:24 2009 +0200
@@ -92,19 +92,11 @@
val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
val trivial: cterm -> thm
- val class_triv: theory -> class -> thm
+ val of_class: ctyp * class -> thm
val unconstrainT: ctyp -> thm -> thm
val dest_state: thm * int -> (term * term) list * term list * term * term
val lift_rule: cterm -> thm -> thm
val incr_indexes: int -> thm -> thm
- val assumption: int -> thm -> thm Seq.seq
- val eq_assumption: int -> thm -> thm
- val rotate_rule: int -> int -> thm -> thm
- val permute_prems: int -> int -> thm -> thm
- val rename_params_rule: string list * int -> thm -> thm
- val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
- val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
- val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
end;
signature THM =
@@ -117,37 +109,46 @@
val dest_fun2: cterm -> cterm
val dest_arg1: cterm -> cterm
val dest_abs: string option -> cterm -> cterm * cterm
- val adjust_maxidx_cterm: int -> cterm -> cterm
val capply: cterm -> cterm -> cterm
val cabs: cterm -> cterm -> cterm
- val major_prem_of: thm -> term
- val no_prems: thm -> bool
+ val adjust_maxidx_cterm: int -> cterm -> cterm
+ val incr_indexes_cterm: int -> cterm -> cterm
+ val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
+ val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
+ val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
val terms_of_tpairs: (term * term) list -> term list
+ val full_prop_of: thm -> term
val maxidx_of: thm -> int
val maxidx_thm: thm -> int -> int
val hyps_of: thm -> term list
- val full_prop_of: thm -> term
+ val no_prems: thm -> bool
+ val major_prem_of: thm -> term
val axiom: theory -> string -> thm
val axioms_of: theory -> (string * thm) list
- val get_name: thm -> string
- val put_name: string -> thm -> thm
val get_tags: thm -> Properties.T
val map_tags: (Properties.T -> Properties.T) -> thm -> thm
val norm_proof: thm -> thm
val adjust_maxidx_thm: int -> thm -> thm
- val rename_boundvars: term -> term -> thm -> thm
- val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
- val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
- val incr_indexes_cterm: int -> cterm -> cterm
val varifyT: thm -> thm
val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
val freezeT: thm -> thm
+ val assumption: int -> thm -> thm Seq.seq
+ val eq_assumption: int -> thm -> thm
+ val rotate_rule: int -> int -> thm -> thm
+ val permute_prems: int -> int -> thm -> thm
+ val rename_params_rule: string list * int -> thm -> thm
+ val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
+ val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
+ val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
+ val rename_boundvars: term -> term -> thm -> thm
val future: thm future -> cterm -> thm
val pending_groups: thm -> Task_Queue.group list -> Task_Queue.group list
val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
val join_proof: thm -> unit
+ val get_name: thm -> string
+ val put_name: string -> thm -> thm
val extern_oracles: theory -> xstring list
val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
end;
@@ -367,6 +368,9 @@
prop = cterm maxidx prop}
end;
+fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) =
+ fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps;
+
fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs [];
fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u';
@@ -473,29 +477,28 @@
(** sort contexts of theorems **)
-fun present_sorts (Thm (_, {hyps, tpairs, prop, ...})) =
- fold (fn (t, u) => Sorts.insert_term t o Sorts.insert_term u) tpairs
- (Sorts.insert_terms hyps (Sorts.insert_term prop []));
-
-(*remove extra sorts that are non-empty by virtue of type signature information*)
+(*remove extra sorts that are witnessed by type signature information*)
fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm
| strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
let
val thy = Theory.deref thy_ref;
- val present = present_sorts thm;
- val extra = Sorts.subtract present shyps;
- val extra' =
- Sorts.subtract (map #2 (Sign.witness_sorts thy present extra)) extra
+ val present =
+ (fold_terms o fold_types o fold_atyps)
+ (fn T as TFree (_, S) => insert (eq_snd op =) (T, S)
+ | T as TVar (_, S) => insert (eq_snd op =) (T, S)) thm [];
+ val extra = fold (Sorts.remove_sort o #2) present shyps;
+ val witnessed = Sign.witness_sorts thy present extra;
+ val extra' = fold (Sorts.remove_sort o #2) witnessed extra
|> Sorts.minimal_sorts (Sign.classes_of thy);
- val shyps' = Sorts.union present extra'
- |> Sorts.remove_sort [];
+ val shyps' = fold (Sorts.insert_sort o #2) present extra';
in
Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
end;
(*dangling sort constraints of a thm*)
-fun extra_shyps (th as Thm (_, {shyps, ...})) = Sorts.subtract (present_sorts th) shyps;
+fun extra_shyps (th as Thm (_, {shyps, ...})) =
+ Sorts.subtract (fold_terms Sorts.insert_term th []) shyps;
@@ -1110,22 +1113,28 @@
tpairs = [],
prop = Logic.mk_implies (A, A)});
-(*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
-fun class_triv thy raw_c =
+(*Axiom-scheme reflecting signature contents
+ T :: c
+ -------------------
+ OFCLASS(T, c_class)
+*)
+fun of_class (cT, raw_c) =
let
+ val Ctyp {thy_ref, T, ...} = cT;
+ val thy = Theory.deref thy_ref;
val c = Sign.certify_class thy raw_c;
- val T = TVar ((Name.aT, 0), [c]);
- val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_inclass (T, c))
- handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
+ val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c));
in
- Thm (deriv_rule0 (Pt.Inclass (T, c)),
- {thy_ref = Theory.check_thy thy,
- tags = [],
- maxidx = maxidx,
- shyps = sorts,
- hyps = [],
- tpairs = [],
- prop = prop})
+ if Sign.of_sort thy (T, [c]) then
+ Thm (deriv_rule0 (Pt.OfClass (T, c)),
+ {thy_ref = Theory.check_thy thy,
+ tags = [],
+ maxidx = maxidx,
+ shyps = sorts,
+ hyps = [],
+ tpairs = [],
+ prop = prop})
+ else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, [])
end;
(*Internalize sort constraints of type variable*)
@@ -1137,7 +1146,7 @@
raise THM ("unconstrainT: not a type variable", 0, [th]);
val T' = TVar ((x, i), []);
val unconstrain = Term.map_types (Term.map_atyps (fn U => if U = T then T' else U));
- val constraints = map (curry Logic.mk_inclass T') S;
+ val constraints = map (curry Logic.mk_of_class T') S;
in
Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
{thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
--- a/src/Pure/type.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Pure/type.ML Tue Jul 07 07:56:24 2009 +0200
@@ -27,7 +27,7 @@
val inter_sort: tsig -> sort * sort -> sort
val cert_class: tsig -> class -> class
val cert_sort: tsig -> sort -> sort
- val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list
+ val witness_sorts: tsig -> (typ * sort) list -> sort list -> (typ * sort) list
type mode
val mode_default: mode
val mode_syntax: mode
--- a/src/Tools/IsaPlanner/isand.ML Mon Jul 06 16:49:51 2009 +0200
+++ b/src/Tools/IsaPlanner/isand.ML Tue Jul 07 07:56:24 2009 +0200
@@ -110,7 +110,7 @@
fun solve_with sol th =
let fun solvei 0 = Seq.empty
| solvei i =
- Seq.append (bicompose false (false,sol,0) i th) (solvei (i - 1))
+ Seq.append (Thm.bicompose false (false,sol,0) i th) (solvei (i - 1))
in
solvei (Thm.nprems_of th)
end;
@@ -337,7 +337,7 @@
val newth' = Drule.implies_intr_list sgallcts allified_newth
in
- bicompose false (false, newth', (length sgallcts)) i gth
+ Thm.bicompose false (false, newth', (length sgallcts)) i gth
end;
(*