# HG changeset patch
# User ballarin
# Date 1227110593 -3600
# Node ID 368aca388dd98dacf37ff6e9eed7a6c29f8060a9
# Parent  6882e110c29ac64204910e68f8d6d3f3e1e12c57
Use 'if' in connection with 'is_some' and 'the'.

diff -r 6882e110c29a -r 368aca388dd9 src/Pure/Isar/new_locale.ML
--- a/src/Pure/Isar/new_locale.ML	Wed Nov 19 17:00:00 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Wed Nov 19 17:03:13 2008 +0100
@@ -222,11 +222,12 @@
       (name', Morphism.identity) :: roundup thy (map fst dependencies);
   in
     input |>
-      not (null params) ? activ_elem (Fixes params) |>
+      (if not (null params) then activ_elem (Fixes params) else I) |>
       (* FIXME type parameters *)
-      is_some asm ? activ_elem (Assumes [(Attrib.no_binding, [(the asm, [])])]) |>
-      not (null defs) ?
-        activ_elem (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs)) |>
+      (if is_some asm then activ_elem (Assumes [(Attrib.no_binding, [(the asm, [])])]) else I) |>
+      (if not (null defs)
+        then activ_elem (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs))
+        else I) |>
       fold_rev (activate_notes activ_elem thy) dependencies'
   end;