--- a/src/HOL/Import/proof_kernel.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Wed Oct 21 00:36:12 2009 +0200
@@ -583,7 +583,7 @@
fun input_types thyname (Elem("tylist",[("i",i)],xtys)) =
let
- val types = Array.array(valOf (Int.fromString i),XMLty (Elem("",[],[])))
+ val types = Array.array(the (Int.fromString i),XMLty (Elem("",[],[])))
fun IT _ [] = ()
| IT n (xty::xtys) =
(Array.update(types,n,XMLty xty);
@@ -650,7 +650,7 @@
fun input_terms thyname types (Elem("tmlist",[("i",i)],xtms)) =
let
- val terms = Array.array(valOf(Int.fromString i),XMLtm (Elem("",[],[])))
+ val terms = Array.array(the (Int.fromString i), XMLtm (Elem("",[],[])))
fun IT _ [] = ()
| IT n (xtm::xtms) =
@@ -1239,7 +1239,7 @@
val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f)
in
if not (idx = "") andalso u = "_"
- then SOME (newstr,valOf(Int.fromString idx))
+ then SOME (newstr, the (Int.fromString idx))
else NONE
end
handle _ => NONE (* FIXME avoid handle _ *)
@@ -1914,7 +1914,7 @@
fun new_definition thyname constname rhs thy =
let
val constname = rename_const thyname thy constname
- val redeclared = isSome (Sign.const_type thy (Sign.intern_const thy constname));
+ val redeclared = is_some (Sign.const_type thy (Sign.intern_const thy constname));
val _ = warning ("Introducing constant " ^ constname)
val (thmname,thy) = get_defname thyname constname thy
val (info,rhs') = disamb_term rhs