src/HOL/Import/proof_kernel.ML
changeset 33035 15eab423e573
parent 32966 5b21661fe618
child 33039 5018f6a76b3f
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Oct 20 23:25:04 2009 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Oct 21 00:36:12 2009 +0200
     1.3 @@ -583,7 +583,7 @@
     1.4  
     1.5  fun input_types thyname (Elem("tylist",[("i",i)],xtys)) =
     1.6      let
     1.7 -        val types = Array.array(valOf (Int.fromString i),XMLty (Elem("",[],[])))
     1.8 +        val types = Array.array(the (Int.fromString i),XMLty (Elem("",[],[])))
     1.9          fun IT _ [] = ()
    1.10            | IT n (xty::xtys) =
    1.11              (Array.update(types,n,XMLty xty);
    1.12 @@ -650,7 +650,7 @@
    1.13  
    1.14  fun input_terms thyname types (Elem("tmlist",[("i",i)],xtms)) =
    1.15      let
    1.16 -        val terms = Array.array(valOf(Int.fromString i),XMLtm (Elem("",[],[])))
    1.17 +        val terms = Array.array(the (Int.fromString i), XMLtm (Elem("",[],[])))
    1.18  
    1.19          fun IT _ [] = ()
    1.20            | IT n (xtm::xtms) =
    1.21 @@ -1239,7 +1239,7 @@
    1.22          val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f)
    1.23      in
    1.24          if not (idx = "") andalso u = "_"
    1.25 -        then SOME (newstr,valOf(Int.fromString idx))
    1.26 +        then SOME (newstr, the (Int.fromString idx))
    1.27          else NONE
    1.28      end
    1.29      handle _ => NONE  (* FIXME avoid handle _ *)
    1.30 @@ -1914,7 +1914,7 @@
    1.31  fun new_definition thyname constname rhs thy =
    1.32      let
    1.33          val constname = rename_const thyname thy constname
    1.34 -        val redeclared = isSome (Sign.const_type thy (Sign.intern_const thy constname));
    1.35 +        val redeclared = is_some (Sign.const_type thy (Sign.intern_const thy constname));
    1.36          val _ = warning ("Introducing constant " ^ constname)
    1.37          val (thmname,thy) = get_defname thyname constname thy
    1.38          val (info,rhs') = disamb_term rhs