misc tuning -- eliminated old-fashioned rep_thm;

--- a/src/HOL/Library/positivstellensatz.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -170,8 +170,8 @@
     Thm.equal_intr (Thm.implies_intr (cprop_of thb) tha) 
      (Thm.implies_intr (cprop_of tha) thb);
 
-fun prove_hyp tha thb = 
-  if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb)) 
+fun prove_hyp tha thb =
+  if exists (curry op aconv (concl_of tha)) (Thm.hyps_of thb)  (* FIXME !? *)
   then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb;
 
 val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and

--- a/src/HOL/Orderings.thy	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/HOL/Orderings.thy	Mon Aug 08 17:23:15 2011 +0200
@@ -531,7 +531,7 @@
 setup {*
 let
 
-fun prp t thm = (#prop (rep_thm thm) = t);
+fun prp t thm = Thm.prop_of thm = t;  (* FIXME aconv!? *)
 
 fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
   let val prems = Simplifier.prems_of ss;

--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -46,7 +46,7 @@
     val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val newTs = take (length (hd descr)) recTs;
 
-    val {maxidx, ...} = rep_thm induct;
+    val maxidx = Thm.maxidx_of induct;
     val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
 
     fun prove_casedist_thm (i, (T, t)) =

--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -270,7 +270,7 @@
 fun lemma thm ct =
   let
     val cu = Z3_Proof_Literals.negate (Thm.dest_arg ct)
-    val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
+    val hyps = map_filter (try HOLogic.dest_Trueprop) (Thm.hyps_of thm)
     val th = Z3_Proof_Tools.under_assumption (intro hyps thm) cu
   in Thm (Z3_Proof_Tools.compose ccontr th) end
 end

--- a/src/HOL/Tools/TFL/rules.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -245,9 +245,7 @@
 
 fun DISJ_CASESL disjth thl =
    let val c = cconcl disjth
-       fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
-                                       aconv term_of atm)
-                              (#hyps(rep_thm th))
+       fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t aconv term_of atm) (Thm.hyps_of th)
        val tml = Dcterm.strip_disj c
        fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"
          | DL th [th1] = PROVE_HYP th th1

--- a/src/HOL/Tools/inductive_codegen.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -581,7 +581,7 @@
         (ks @ [SOME k]))) arities));
 
 fun prep_intrs intrs =
-  map (Codegen.rename_term o #prop o rep_thm o Drule.export_without_context) intrs;
+  map (Codegen.rename_term o Thm.prop_of o Drule.export_without_context) intrs;
 
 fun constrain cs [] = []
   | constrain cs ((s, xs) :: ys) =

--- a/src/HOL/Tools/sat_funcs.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -153,11 +153,13 @@
         fun resolution (c1, hyps1) (c2, hyps2) =
           let
             val _ =
-              if ! trace_sat then
+              if ! trace_sat then  (* FIXME !? *)
                 tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
-                  " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
+                  " (hyps: " ^ ML_Syntax.print_list
+                    (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1)
                   ^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
-                  " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
+                  " (hyps: " ^ ML_Syntax.print_list
+                    (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")")
               else ()
 
             (* the two literals used for resolution *)
@@ -189,7 +191,7 @@
               if !trace_sat then
                 tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
                   " (hyps: " ^ ML_Syntax.print_list
-                      (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
+                      (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")")
               else ()
             val _ = Unsynchronized.inc counter
           in

--- a/src/Provers/hypsubst.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/Provers/hypsubst.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -116,8 +116,7 @@
 (*For the simpset.  Adds ALL suitable equalities, even if not first!
   No vars are allowed here, as simpsets are built from meta-assumptions*)
 fun mk_eqs bnd th =
-    [ if inspect_pair bnd false (Data.dest_eq
-                                   (Data.dest_Trueprop (#prop (rep_thm th))))
+    [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th)))
       then th RS Data.eq_reflection
       else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
     handle TERM _ => [] | Match => [];

--- a/src/Pure/Isar/element.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/Pure/Isar/element.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -266,7 +266,7 @@
 
 val mark_witness = Logic.protect;
 fun witness_prop (Witness (t, _)) = t;
-fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th);
+fun witness_hyps (Witness (_, th)) = Thm.hyps_of th;
 fun map_witness f (Witness witn) = Witness (f witn);
 
 fun morph_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));

--- a/src/Pure/Isar/rule_insts.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -312,7 +312,7 @@
               (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
               (xis ~~ ts));
         (* Lift and instantiate rule *)
-        val {maxidx, ...} = rep_thm st;
+        val maxidx = Thm.maxidx_of st;
         val paramTs = map #2 params
         and inc = maxidx+1
         fun liftvar (Var ((a,j), T)) =

--- a/src/Pure/Proof/proofchecker.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/Pure/Proof/proofchecker.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -86,7 +86,7 @@
     fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
           let
             val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
-            val {prop, ...} = rep_thm thm;
+            val prop = Thm.prop_of thm;
             val _ =
               if is_equal prop prop' then ()
               else

--- a/src/Pure/raw_simplifier.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/Pure/raw_simplifier.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -1197,7 +1197,7 @@
               val prem' = Thm.rhs_of eqn;
               val tprems = map term_of prems;
               val i = 1 + fold Integer.max (map (fn p =>
-                find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
+                find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1;
               val (rrs', asm') = rules_of_prem ss prem'
             in mut_impc prems concl rrss asms (prem' :: prems')
               (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)

--- a/src/Pure/simplifier.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/Pure/simplifier.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -410,7 +410,7 @@
       if can Logic.dest_equals (Thm.concl_of thm) then [thm]
       else [thm RS reflect] handle THM _ => [];
 
-    fun mksimps thm = mk_eq (Thm.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
+    fun mksimps thm = mk_eq (Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm);
   in
     empty_ss setsubgoaler asm_simp_tac
     setSSolver safe_solver

--- a/src/ZF/Tools/datatype_package.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -339,7 +339,7 @@
       end
 
   val constructors =
-      map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
+      map (head_of o #1 o Logic.dest_equals o Thm.prop_of) (tl con_defs);
 
   val free_SEs = map Drule.export_without_context (Ind_Syntax.mk_free_SEs free_iffs);
 

--- a/src/ZF/Tools/induct_tacs.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -123,8 +123,7 @@
                               Syntax.string_of_term_global thy eqn);
 
     val constructors =
-        map (head_of o const_of o FOLogic.dest_Trueprop o
-             #prop o rep_thm) case_eqns;
+        map (head_of o const_of o FOLogic.dest_Trueprop o Thm.prop_of) case_eqns;
 
     val Const (@{const_name mem}, _) $ _ $ data =
         FOLogic.dest_Trueprop (hd (prems_of elim));

--- a/src/ZF/arith_data.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/ZF/arith_data.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -61,7 +61,7 @@
 (*We remove equality assumptions because they confuse the simplifier and
   because only type-checking assumptions are necessary.*)
 fun is_eq_thm th =
-    can FOLogic.dest_eq (FOLogic.dest_Trueprop (#prop (rep_thm th)));
+    can FOLogic.dest_eq (FOLogic.dest_Trueprop (Thm.prop_of th));
 
 fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
 
@@ -69,7 +69,7 @@
   if t aconv u then NONE
   else
   let val prems' = filter_out is_eq_thm prems
-      val goal = Logic.list_implies (map (#prop o Thm.rep_thm) prems',
+      val goal = Logic.list_implies (map Thm.prop_of prems',
         FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
   in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs)))
       handle ERROR msg =>