src/HOL/Library/old_recdef.ML
changeset 60949 ccbf9379e355
parent 60825 bacfb7c45d81
child 61038 9c28a4feebd1
--- 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 =