diff -r 8ac3803c8f73 -r 5fd94d84470f src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue May 17 10:19:44 2005 +0200
@@ -241,10 +241,10 @@
 
 fun error_var msg xi = error (msg ^ Syntax.string_of_vname xi);
 
-fun the_sort sorts xi = valOf (sorts xi)
+fun the_sort sorts xi = the (sorts xi)
   handle Option.Option => error_var "No such type variable in theorem: " xi;
 
-fun the_type types xi = valOf (types xi)
+fun the_type types xi = the (types xi)
   handle Option.Option => error_var "No such variable in theorem: " xi;
 
 fun unify_types sign types ((unifier, maxidx), (xi, u)) =
@@ -339,9 +339,9 @@
 
     mixed_insts |> List.app (fn (arg, (xi, _)) =>
       if is_tvar xi then
-        Args.assign (SOME (Args.Typ (valOf (assoc (type_insts''', xi))))) arg
+        Args.assign (SOME (Args.Typ (the (assoc (type_insts''', xi))))) arg
       else
-        Args.assign (SOME (Args.Term (valOf (assoc (term_insts''', xi))))) arg);
+        Args.assign (SOME (Args.Term (the (assoc (term_insts''', xi))))) arg);
 
     (context, thm''' |> RuleCases.save thm)
   end;