Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/indrule.ML
changeset 2270 d7513875b2b8
parent 2031 03a843f0f447
child 2637 e9b203f854ae 
--- a/src/HOL/indrule.ML	Thu Nov 28 12:28:52 1996 +0100
+++ b/src/HOL/indrule.ML	Thu Nov 28 12:31:33 1996 +0100
@@ -143,7 +143,7 @@
        (big_rec_tm,
         Abs("z", elem_type, 
             fold_bal (app Ind_Syntax.conj) 
-            (map mk_rec_imp (Inductive.rec_tms~~preds)))))
+            (ListPair.map mk_rec_imp (Inductive.rec_tms,preds)))))
 and mutual_induct_concl = 
     Ind_Syntax.mk_Trueprop (fold_bal (app Ind_Syntax.conj) qconcls);
isabelle