--- 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;