src/HOL/Tools/datatype_rep_proofs.ML
changeset 8305 93aa21ec5494
parent 8005 b64d86018785
child 8436 8a87fa482baf
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Sun Feb 27 15:25:31 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sun Feb 27 15:26:47 2000 +0100
     1.3 @@ -623,7 +623,7 @@
     1.4                [TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1,
     1.5                 etac mp 1, resolve_tac iso_elem_thms 1])]);
     1.6  
     1.7 -    val Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
     1.8 +    val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
     1.9      val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
    1.10        map (Free o apfst fst o dest_Var) Ps;
    1.11      val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;