--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Fri Aug 28 11:52:06 2015 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Fri Aug 28 11:53:09 2015 +0200
@@ -191,12 +191,8 @@
datatype cthm = ComputeThm of term list * sort list * term
fun thm2cthm th =
- let
- val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th
- val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else ()
- in
- ComputeThm (hyps, shyps, prop)
- end
+ (if not (null (Thm.tpairs_of th)) then raise Make "theorems may not contain tpairs" else ();
+ ComputeThm (Thm.hyps_of th, Thm.shyps_of th, Thm.prop_of th))
fun make_internal machine thy stamp encoding cache_pattern_terms raw_ths =
let
--- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Fri Aug 28 11:52:06 2015 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Fri Aug 28 11:53:09 2015 +0200
@@ -367,16 +367,13 @@
datatype cthm = ComputeThm of term list * sort list * term
-fun thm2cthm th =
- let
- val {hyps, prop, shyps, ...} = Thm.rep_thm th
- in
- ComputeThm (hyps, shyps, prop)
- end
+fun thm2cthm th = ComputeThm (Thm.hyps_of th, Thm.shyps_of th, Thm.prop_of th)
-val cthm_ord' = prod_ord (prod_ord (list_ord Term_Ord.term_ord) (list_ord Term_Ord.sort_ord)) Term_Ord.term_ord
+val cthm_ord' =
+ prod_ord (prod_ord (list_ord Term_Ord.term_ord) (list_ord Term_Ord.sort_ord)) Term_Ord.term_ord
-fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
+fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) =
+ cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
structure CThmtab = Table(type key = cthm val ord = cthm_ord)
--- a/src/HOL/Proofs/ex/XML_Data.thy Fri Aug 28 11:52:06 2015 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy Fri Aug 28 11:53:09 2015 +0200
@@ -14,8 +14,9 @@
ML {*
fun export_proof thy thm =
let
- val {prop, hyps, shyps, ...} = Thm.rep_thm thm;
- val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop));
+ val (_, prop) =
+ Logic.unconstrainT (Thm.shyps_of thm)
+ (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
val prf =
Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |>
Reconstruct.reconstruct_proof thy prop |>
--- a/src/Pure/Proof/extraction.ML Fri Aug 28 11:52:06 2015 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Aug 28 11:53:09 2015 +0200
@@ -364,7 +364,7 @@
let
val S = Sign.defaultS thy;
val ((atyp_map, constraints, _), prop') =
- Logic.unconstrainT (#shyps (Thm.rep_thm thm)) (Thm.prop_of thm);
+ Logic.unconstrainT (Thm.shyps_of thm) (Thm.prop_of thm);
val atyps = fold_types (fold_atyps (insert (op =))) (Thm.prop_of thm) [];
val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then
SOME (TVar (("'" ^ v, i), [])) else NONE)
--- a/src/Pure/display.ML Fri Aug 28 11:52:06 2015 +0200
+++ b/src/Pure/display.ML Fri Aug 28 11:53:09 2015 +0200
@@ -52,27 +52,28 @@
val show_hyps = Config.get ctxt show_hyps;
val th = Thm.strip_shyps raw_th;
- val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
- val hyps' = if show_hyps then hyps else Thm.undeclared_hyps (Context.Proof ctxt) th;
+
+ val hyps = if show_hyps then Thm.hyps_of th else Thm.undeclared_hyps (Context.Proof ctxt) th;
val extra_shyps = Thm.extra_shyps th;
val tags = Thm.get_tags th;
+ val tpairs = Thm.tpairs_of th;
val q = if quote then Pretty.quote else I;
val prt_term = q o Syntax.pretty_term ctxt;
- val hlen = length extra_shyps + length hyps' + length tpairs;
+ val hlen = length extra_shyps + length hyps + length tpairs;
val hsymbs =
if hlen = 0 then []
else if show_hyps orelse show_hyps' then
[Pretty.brk 2, Pretty.list "[" "]"
- (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
+ (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps @
map (Syntax.pretty_sort ctxt) extra_shyps)]
else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
val tsymbs =
if null tags orelse not show_tags then []
else [Pretty.brk 1, pretty_tags tags];
- in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
+ in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end;
fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true};
fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th];
--- a/src/Pure/goal_display.ML Fri Aug 28 11:52:06 2015 +0200
+++ b/src/Pure/goal_display.ML Fri Aug 28 11:53:09 2015 +0200
@@ -114,7 +114,7 @@
val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
- val {prop, tpairs, ...} = Thm.rep_thm state;
+ val prop = Thm.prop_of state;
val (As, B) = Logic.strip_horn prop;
val ngoals = length As;
in
@@ -124,7 +124,7 @@
pretty_subgoals (take goals_limit As) @
[Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
else pretty_subgoals As) @
- pretty_ffpairs tpairs @
+ pretty_ffpairs (Thm.tpairs_of state) @
(if show_consts then pretty_consts prop else []) @
(if show_types then pretty_vars prop else []) @
(if show_sorts0 then pretty_varsT prop else [])
--- a/src/Pure/more_thm.ML Fri Aug 28 11:52:06 2015 +0200
+++ b/src/Pure/more_thm.ML Fri Aug 28 11:53:09 2015 +0200
@@ -161,21 +161,19 @@
(* thm order: ignores theory context! *)
-fun thm_ord (th1, th2) =
- let
- val {shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = Thm.rep_thm th1;
- val {shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = Thm.rep_thm th2;
- in
- (case Term_Ord.fast_term_ord (prop1, prop2) of
- EQUAL =>
- (case list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) (tpairs1, tpairs2) of
- EQUAL =>
- (case list_ord Term_Ord.fast_term_ord (hyps1, hyps2) of
- EQUAL => list_ord Term_Ord.sort_ord (shyps1, shyps2)
- | ord => ord)
- | ord => ord)
- | ord => ord)
- end;
+fun thm_ord ths =
+ (case Term_Ord.fast_term_ord (apply2 Thm.prop_of ths) of
+ EQUAL =>
+ (case
+ list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord)
+ (apply2 Thm.tpairs_of ths)
+ of
+ EQUAL =>
+ (case list_ord Term_Ord.fast_term_ord (apply2 Thm.hyps_of ths) of
+ EQUAL => list_ord Term_Ord.sort_ord (apply2 Thm.shyps_of ths)
+ | ord => ord)
+ | ord => ord)
+ | ord => ord);
(* tables and caches *)
@@ -240,15 +238,14 @@
let
val thm = Thm.strip_shyps raw_thm;
fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]);
- val {hyps, prop, tpairs, ...} = Thm.rep_thm thm;
in
- if not (null hyps) then
+ if not (null (Thm.hyps_of thm)) then
err "theorem may not contain hypotheses"
else if not (null (Thm.extra_shyps thm)) then
err "theorem may not contain sort hypotheses"
- else if not (null tpairs) then
+ else if not (null (Thm.tpairs_of thm)) then
err "theorem may not contain flex-flex pairs"
- else prop
+ else Thm.prop_of thm
end;
--- a/src/Pure/thm.ML Fri Aug 28 11:52:06 2015 +0200
+++ b/src/Pure/thm.ML Fri Aug 28 11:53:09 2015 +0200
@@ -70,6 +70,7 @@
val theory_name_of_thm: thm -> string
val maxidx_of: thm -> int
val maxidx_thm: thm -> int -> int
+ val shyps_of: thm -> sort Ord_List.T
val hyps_of: thm -> term list
val prop_of: thm -> term
val tpairs_of: thm -> (term * term) list
@@ -412,6 +413,7 @@
val maxidx_of = #maxidx o rep_thm;
fun maxidx_thm th i = Int.max (maxidx_of th, i);
+val shyps_of = #shyps o rep_thm;
val hyps_of = #hyps o rep_thm;
val prop_of = #prop o rep_thm;
val tpairs_of = #tpairs o rep_thm;