--- a/src/Pure/Isar/object_logic.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/src/Pure/Isar/object_logic.ML Thu Mar 03 12:43:01 2005 +0100
@@ -48,7 +48,7 @@
fun merge_judgment (SOME x, SOME y) =
if x = y then SOME x else error "Attempt to merge different object-logics"
- | merge_judgment (j1, j2) = if is_some j1 then j1 else j2;
+ | merge_judgment (j1, j2) = if isSome j1 then j1 else j2;
fun merge ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
(merge_judgment (judgment1, judgment2),
@@ -116,7 +116,7 @@
val c = judgment_name sg;
val aT = TFree ("'a", []);
val T =
- if_none (Sign.const_type sg c) (aT --> propT)
+ getOpt (Sign.const_type sg c, aT --> propT)
|> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
val U = Term.domain_type T handle Match => aT;
in Const (c, T) $ Free (x, U) end;