src/HOL/Bali/Eval.thy
changeset 12919 d6a0d168291e
parent 12858 6214f03d6d27
child 12925 99131847fb93
     1.1 --- a/src/HOL/Bali/Eval.thy	Thu Feb 21 20:08:09 2002 +0100
     1.2 +++ b/src/HOL/Bali/Eval.thy	Thu Feb 21 20:09:19 2002 +0100
     1.3 @@ -779,7 +779,7 @@
     1.4  
     1.5  ML {*
     1.6  local
     1.7 -  fun is_None (Const ("Option.option.None",_)) = true
     1.8 +  fun is_None (Const ("Datatype.option.None",_)) = true
     1.9      | is_None _ = false
    1.10    fun pred (t as (_ $ (Const ("Pair",_) $
    1.11       (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x
    1.12 @@ -806,7 +806,7 @@
    1.13  
    1.14  ML {*
    1.15  local
    1.16 -  fun is_Some (Const ("Pair",_) $ (Const ("Option.option.Some",_) $ _)$ _) =true
    1.17 +  fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
    1.18      | is_Some _ = false
    1.19    fun pred (_ $ (Const ("Pair",_) $
    1.20       _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $