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/intr_elim.ML
changeset 2270 d7513875b2b8
parent 2031 03a843f0f447
child 2414 13df7d6c5c3b 
--- a/src/HOL/intr_elim.ML	Thu Nov 28 12:28:52 1996 +0100
+++ b/src/HOL/intr_elim.ML	Thu Nov 28 12:31:33 1996 +0100
@@ -100,8 +100,8 @@
         and g rl = rl RS disjI2
     in  accesses_bal(f, g, asm_rl)  end;
 
-val intrs = map (uncurry (prove_goalw_cterm part_rec_defs))
-            (map (cterm_of sign) Inductive.intr_tms ~~ 
+val intrs = ListPair.map (uncurry (prove_goalw_cterm part_rec_defs))
+            (map (cterm_of sign) Inductive.intr_tms,
              map intro_tacsf (mk_disj_rls(length Inductive.intr_tms)));
 
 (********)
isabelle