Use 'if' in connection with 'is_some' and 'the'.
authorballarin
Wed, 19 Nov 2008 17:03:13 +0100
changeset 28851 368aca388dd9
parent 28850 6882e110c29a
child 28852 5ddea758679b
Use 'if' in connection with 'is_some' and 'the'.
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;