# HG changeset patch
# User wenzelm
# Date 1439745908 -7200
# Node ID ccbf9379e355583ebb9efce4220724559a5273a4
# Parent  b710a5087116ca7edb9e97672d2000bb4fc7ea36
added Thm.chyps_of;
eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);

diff -r b710a5087116 -r ccbf9379e355 src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -400,7 +400,7 @@
   let
     val ident = Thm.cterm_of ctxt (HOLogic.mk_number @{typ nat} ident |> Logic.mk_term);
     val hyp =
-      (case #hyps (Thm.crep_thm prem) of
+      (case Thm.chyps_of prem of
         [hyp] => hyp
       | _ => error "Prem should have exactly one hyp");  (* FIXME error vs. raise Fail !? *)
     val ct = Drule.mk_term (hyp) |> Thm.cprop_of;
@@ -455,7 +455,7 @@
 
 fun get_thinned_prems goal =
   let
-    val chyps = Thm.crep_thm goal |> #hyps;
+    val chyps = Thm.chyps_of goal;
 
     fun prem_from_hyp hyp goal =
     let
@@ -735,7 +735,7 @@
                     (focus_prems inner_ctxt |> snd |> Item_Net.content)
                     (focus_prems focus_ctxt |> snd |> Item_Net.content))
                     |> map (fn (id, thm) =>
-                        #hyps (Thm.crep_thm thm)
+                        Thm.chyps_of thm
                         |> (fn [chyp] => (id, (SOME chyp, NONE))
                              | _ => error "Prem should have only one hyp")));
 
diff -r b710a5087116 -r ccbf9379e355 src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -694,7 +694,7 @@
     Old_Z3_Proof_Tools.with_conv unfold_conv Old_Z3_Proof_Literals.prove_conj_disj_eq
 
   fun declare_hyps ctxt thm =
-    (thm, snd (Assumption.add_assumes (#hyps (Thm.crep_thm thm)) ctxt))
+    (thm, snd (Assumption.add_assumes (Thm.chyps_of thm) ctxt))
 in
 
 val abstraction_depth = 3
diff -r b710a5087116 -r ccbf9379e355 src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -914,8 +914,8 @@
 fun RULES_ERR func mesg = Utils.ERR {module = "Rules", func = func, mesg = mesg};
 
 
-fun cconcl thm = Dcterm.drop_prop (#prop (Thm.crep_thm thm));
-fun chyps thm = map Dcterm.drop_prop (#hyps (Thm.crep_thm thm));
+fun cconcl thm = Dcterm.drop_prop (Thm.cprop_of thm);
+fun chyps thm = map Dcterm.drop_prop (Thm.chyps_of thm);
 
 fun dest_thm thm =
   let val {prop,hyps,...} = Thm.rep_thm thm
@@ -971,7 +971,7 @@
 fun DISCH tm thm = Thm.implies_intr (Dcterm.mk_prop tm) thm COMP impI
   handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
 
-fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm;
+fun DISCH_ALL thm = fold_rev DISCH (Thm.chyps_of thm) thm;
 
 
 fun FILTER_DISCH_ALL P thm =
diff -r b710a5087116 -r ccbf9379e355 src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -540,7 +540,7 @@
     fun simple_choose v th =
       choose v
         (Thm.assume
-          ((Thm.apply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
+          ((Thm.apply @{cterm Trueprop} o mk_ex v) (Thm.dest_arg (hd (Thm.chyps_of th))))) th
 
     val strip_forall =
       let
diff -r b710a5087116 -r ccbf9379e355 src/HOL/Multivariate_Analysis/normarith.ML
--- a/src/HOL/Multivariate_Analysis/normarith.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -354,7 +354,7 @@
   val gts' = map replace_rule gts
   val nubs = map (conjunct2 o norm_mp) asl
   val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts')
-  val shs = filter (member (fn (t,th) => t aconvc Thm.cprop_of th) asl) (#hyps (Thm.crep_thm th1))
+  val shs = filter (member (fn (t,th) => t aconvc Thm.cprop_of th) asl) (Thm.chyps_of th1)
   val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
   val cps = map (swap o Thm.dest_equals) (cprems_of th11)
   val th12 = Drule.instantiate_normalize ([], map (apfst (dest_Var o Thm.term_of)) cps) th11
diff -r b710a5087116 -r ccbf9379e355 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -182,7 +182,7 @@
       | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
       | _ => raise General.Fail "Too many conditions"
 
-    val simp_ctxt = fold Thm.declare_hyps (#hyps (Thm.crep_thm simp)) ctxt
+    val simp_ctxt = fold Thm.declare_hyps (Thm.chyps_of simp) ctxt
   in
     Goal.prove simp_ctxt [] []
       (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
diff -r b710a5087116 -r ccbf9379e355 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -433,7 +433,7 @@
         val (prems0, concl) = th |> Thm.prop_of |> Logic.strip_horn
         val prems = prems0 |> map normalize_literal |> distinct Term.aconv_untyped
         val goal = Logic.list_implies (prems, concl)
-        val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm th)) ctxt
+        val ctxt' = fold Thm.declare_hyps (Thm.chyps_of th) ctxt
         val tac =
           cut_tac th 1 THEN
           rewrite_goals_tac ctxt' meta_not_not THEN
@@ -727,7 +727,7 @@
       val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
                        cat_lines (map string_of_subst_info substs))
 *)
-      val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm prems_imp_false)) ctxt
+      val ctxt' = fold Thm.declare_hyps (Thm.chyps_of prems_imp_false) ctxt
 
       fun cut_and_ex_tac axiom =
         cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (eresolve_tac ctxt' @{thms exE}) 1)
diff -r b710a5087116 -r ccbf9379e355 src/HOL/Tools/SMT/z3_replay_methods.ML
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -522,7 +522,7 @@
 
 fun lemma ctxt (thms as [thm]) t =
     (let
-       val tab = Termtab.make (map (`Thm.term_of) (#hyps (Thm.crep_thm thm)))
+       val tab = Termtab.make (map (`Thm.term_of) (Thm.chyps_of thm))
        val (thm', terms) = intro_hyps tab (dest_prop t) (thm, [])
      in
        prove_abstract ctxt [thm'] t prop_tac (
diff -r b710a5087116 -r ccbf9379e355 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/HOL/Tools/groebner.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -496,7 +496,7 @@
 
 fun simple_choose v th =
    choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v)
-    ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
+    (Thm.dest_arg (hd (Thm.chyps_of th))))) th
 
 
  fun mkexi v th =
diff -r b710a5087116 -r ccbf9379e355 src/HOL/Tools/sat.ML
--- a/src/HOL/Tools/sat.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/HOL/Tools/sat.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -226,7 +226,7 @@
             val _ = cond_tracing ctxt (fn () => "Using original clause #" ^ string_of_int id)
             val raw = CNF.clause2raw_thm ctxt thm
             val hyps = sort (lit_ord o apply2 fst) (map_filter (fn chyp =>
-              Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw)))
+              Option.map (rpair chyp) (index_of_literal chyp)) (Thm.chyps_of raw))
             val clause = (raw, hyps)
             val _ = Array.update (clauses, id, RAW_CLAUSE clause)
           in
diff -r b710a5087116 -r ccbf9379e355 src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Sun Aug 16 19:25:08 2015 +0200
@@ -37,7 +37,7 @@
     val horns25 = Meson.make_horns clauses25;     (*16 Horn clauses*)
     val go25 :: _ = Meson.gocls clauses25;
 
-    val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt;
+    val ctxt' = fold Thm.declare_hyps (maps Thm.chyps_of (go25 :: horns25)) ctxt;
     Goal.prove ctxt' [] [] @{prop False} (fn _ =>
       resolve_tac ctxt' [go25] 1 THEN
       Meson.depth_prolog_tac ctxt' horns25);
@@ -63,7 +63,7 @@
     val _ = @{assert} (length horns26 = 24);
     val go26 :: _ = Meson.gocls clauses26;
 
-    val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go26 :: horns26)) ctxt;
+    val ctxt' = fold Thm.declare_hyps (maps Thm.chyps_of (go26 :: horns26)) ctxt;
     Goal.prove ctxt' [] [] @{prop False} (fn _ =>
       resolve_tac ctxt' [go26] 1 THEN
       Meson.depth_prolog_tac ctxt' horns26);  (*7 ms*)
@@ -90,7 +90,7 @@
     val _ = @{assert} (length horns43 = 16);
     val go43 :: _ = Meson.gocls clauses43;
 
-    val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go43 :: horns43)) ctxt;
+    val ctxt' = fold Thm.declare_hyps (maps Thm.chyps_of (go43 :: horns43)) ctxt;
     Goal.prove ctxt' [] [] @{prop False} (fn _ =>
       resolve_tac ctxt' [go43] 1 THEN
       Meson.best_prolog_tac ctxt' Meson.size_of_subgoals horns43);   (*7ms*)
diff -r b710a5087116 -r ccbf9379e355 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/Pure/Isar/code.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -686,7 +686,7 @@
 
 fun get_head thy cert_thm =
   let
-    val [head] = (#hyps o Thm.crep_thm) cert_thm;
+    val [head] = Thm.chyps_of cert_thm;
     val (_, Const (c, ty)) = (Logic.dest_equals o Thm.term_of) head;
   in (typscheme thy (c, ty), head) end;
 
diff -r b710a5087116 -r ccbf9379e355 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/Pure/Isar/element.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -359,7 +359,7 @@
   Drule.forall_elim_list (map (Thm.global_cterm_of thy o snd) subst);
 
 fun hyps_rule rule th =
-  let val {hyps, ...} = Thm.crep_thm th in
+  let val hyps = Thm.chyps_of th in
     Drule.implies_elim_list
       (rule (Drule.implies_intr_list hyps th))
       (map (Thm.assume o Drule.cterm_rule rule) hyps)
@@ -452,7 +452,7 @@
   thm |> fold (fn hyp =>
     (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of
       NONE => I
-    | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm));
+    | SOME w => Thm.implies_intr hyp #> compose_witness w)) (Thm.chyps_of thm);
 
 val satisfy_morphism = Morphism.thm_morphism "Element.satisfy" o satisfy_thm;
 
diff -r b710a5087116 -r ccbf9379e355 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/Pure/Isar/expression.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -702,7 +702,7 @@
       |> Conjunction.elim_balanced (length ts);
 
     val (_, axioms_ctxt) = defs_ctxt
-      |> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts));
+      |> Assumption.add_assumes (maps Thm.chyps_of (defs @ conjuncts));
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
       Element.prove_witness axioms_ctxt t
        (rewrite_goals_tac axioms_ctxt defs THEN compose_tac axioms_ctxt (false, ax, 0) 1));
diff -r b710a5087116 -r ccbf9379e355 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -54,7 +54,7 @@
       error "Conclusion in obtained context must be object-logic judgment";
 
     val ((_, [thm']), ctxt') = Variable.import true [thm] ctxt;
-    val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm'));
+    val prems = Drule.strip_imp_prems (Thm.cprop_of thm');
   in
     ((Drule.implies_elim_list thm' (map Thm.assume prems)
         |> Drule.implies_intr_list (map (Drule.norm_hhf_cterm ctxt') As)
diff -r b710a5087116 -r ccbf9379e355 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/Pure/drule.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -233,8 +233,7 @@
     Frees, or outer quantifiers; all generality expressed by Vars of index 0.**)
 
 (*Discharge all hypotheses.*)
-fun implies_intr_hyps th =
-  fold Thm.implies_intr (#hyps (Thm.crep_thm th)) th;
+fun implies_intr_hyps th = fold Thm.implies_intr (Thm.chyps_of th) th;
 
 (*Squash a theorem's flexflex constraints provided it can be done uniquely.
   This step can lose information.*)
diff -r b710a5087116 -r ccbf9379e355 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Aug 16 18:19:30 2015 +0200
+++ b/src/Pure/thm.ML	Sun Aug 16 19:25:08 2015 +0200
@@ -58,14 +58,6 @@
     hyps: term Ord_List.T,
     tpairs: (term * term) list,
     prop: term}
-  val crep_thm: thm ->
-   {thy: theory,
-    tags: Properties.T,
-    maxidx: int,
-    shyps: sort Ord_List.T,
-    hyps: cterm Ord_List.T,
-    tpairs: (cterm * cterm) list,
-    prop: cterm}
   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
   val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
   val terms_of_tpairs: (term * term) list -> term list
@@ -85,6 +77,7 @@
   val major_prem_of: thm -> term
   val cprop_of: thm -> cterm
   val cprem_of: thm -> int -> cterm
+  val chyps_of: thm -> cterm list
   val transfer: theory -> thm -> thm
   val renamed_prop: term -> thm -> thm
   val weaken: cterm -> thm -> thm
@@ -353,14 +346,6 @@
 
 fun rep_thm (Thm (_, args)) = args;
 
-fun crep_thm (Thm (_, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) =
-  let fun cterm max t = Cterm {thy = thy, t = t, T = propT, maxidx = max, sorts = shyps} in
-   {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps,
-    hyps = map (cterm ~1) hyps,
-    tpairs = map (apply2 (cterm maxidx)) tpairs,
-    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;
 
@@ -420,7 +405,6 @@
     prem :: _ => Logic.strip_assums_concl prem
   | [] => raise THM ("major_prem_of: rule with no premises", 0, [th]));
 
-(*the statement of any thm is a cterm*)
 fun cprop_of (Thm (_, {thy, maxidx, shyps, prop, ...})) =
   Cterm {thy = thy, maxidx = maxidx, T = propT, t = prop, sorts = shyps};
 
@@ -428,6 +412,9 @@
   Cterm {thy = thy, maxidx = maxidx, T = propT, sorts = shyps,
     t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])};
 
+fun chyps_of (Thm (_, {thy, shyps, hyps, ...})) =
+  map (fn t => Cterm {thy = thy, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps;
+
 (*explicit transfer to a super theory*)
 fun transfer thy' thm =
   let