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/Provers/Arith/cancel_numeral_factor.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15965 f422f8283491 
--- a/src/Provers/Arith/cancel_numeral_factor.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/Provers/Arith/cancel_numeral_factor.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -75,7 +75,7 @@
 	    Data.prove_conv [Data.norm_tac] sg hyps xs
 	      (t',   Data.mk_bal (newshape(n1,t1'), newshape(n2,t2')))
   in
-      apsome Data.simplify_meta_eq
+      Option.map Data.simplify_meta_eq
        (Data.prove_conv 
 	       [Data.trans_tac reshape, rtac Data.cancel 1,
 		Data.numeral_simp_tac] sg hyps xs (t', rhs))
isabelle