src/HOL/Tools/datatype_realizer.ML
changeset 59058 a78612c67ec0
parent 58963 26bf09b95dda
child 59498 50b60f501b05
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -106,7 +106,7 @@
     1.4          (map (fn ((((i, _), T), U), tname) =>
     1.5            make_pred i U T (mk_proj i is r) (Free (tname, T)))
     1.6              (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
     1.7 -    val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
     1.8 +    val inst = map (apply2 cert) (map head_of (HOLogic.dest_conj
     1.9        (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
    1.10  
    1.11      val thm =