# HG changeset patch # User wenzelm # Date 1312816995 -7200 # Node ID ae85c5d64913050e7d3565634e4164af1b8eac0f # Parent fda143b5c2f559385b485dd7290f5489fc4f0215 misc tuning -- eliminated old-fashioned rep_thm; diff -r fda143b5c2f5 -r ae85c5d64913 src/HOL/Library/positivstellensatz.ML --- 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 diff -r fda143b5c2f5 -r ae85c5d64913 src/HOL/Orderings.thy --- 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; diff -r fda143b5c2f5 -r ae85c5d64913 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- 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)) = diff -r fda143b5c2f5 -r ae85c5d64913 src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- 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 diff -r fda143b5c2f5 -r ae85c5d64913 src/HOL/Tools/TFL/rules.ML --- 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 diff -r fda143b5c2f5 -r ae85c5d64913 src/HOL/Tools/inductive_codegen.ML --- 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) = diff -r fda143b5c2f5 -r ae85c5d64913 src/HOL/Tools/sat_funcs.ML --- 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 diff -r fda143b5c2f5 -r ae85c5d64913 src/Provers/hypsubst.ML --- 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 => []; diff -r fda143b5c2f5 -r ae85c5d64913 src/Pure/Isar/element.ML --- 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)); diff -r fda143b5c2f5 -r ae85c5d64913 src/Pure/Isar/rule_insts.ML --- 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)) = diff -r fda143b5c2f5 -r ae85c5d64913 src/Pure/Proof/proofchecker.ML --- 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 diff -r fda143b5c2f5 -r ae85c5d64913 src/Pure/raw_simplifier.ML --- 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) diff -r fda143b5c2f5 -r ae85c5d64913 src/Pure/simplifier.ML --- 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 diff -r fda143b5c2f5 -r ae85c5d64913 src/ZF/Tools/datatype_package.ML --- 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); diff -r fda143b5c2f5 -r ae85c5d64913 src/ZF/Tools/induct_tacs.ML --- 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)); diff -r fda143b5c2f5 -r ae85c5d64913 src/ZF/arith_data.ML --- 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 =>