src/Pure/Isar/find_theorems.ML
changeset 17756 d4a35f82fbb4
parent 17755 b0cd55afead1
child 17789 ccba4e900023
--- a/src/Pure/Isar/find_theorems.ML	Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Tue Oct 04 19:01:37 2005 +0200
@@ -218,7 +218,7 @@
 
 fun opt_not x = if isSome x then NONE else SOME (0, 0);
 
-fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y)
+fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int)
  |  opt_add _ _ = NONE;
 
 in