src/HOL/Tools/datatype_abs_proofs.ML
changeset 8305 93aa21ec5494
parent 7904 2b551893583e
child 8436 8a87fa482baf
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Sun Feb 27 15:25:31 2000 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sun Feb 27 15:26:47 2000 +0100
@@ -62,7 +62,7 @@
     val recTs = get_rec_types descr' sorts;
     val newTs = take (length (hd descr), recTs);
 
-    val induct_Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
+    val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
 
     fun prove_casedist_thm ((i, t), T) =
       let
@@ -109,7 +109,7 @@
     val used = foldr add_typ_tfree_names (recTs, []);
     val newTs = take (length (hd descr), recTs);
 
-    val induct_Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
+    val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
 
     val big_rec_name' = big_name ^ "_rec_set";
     val rec_set_names = map (Sign.full_name (Theory.sign_of thy0))