diff -r 11095c312709 -r 8e71b9228d2d src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Mon Nov 21 19:52:50 2011 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Mon Nov 21 21:38:08 2011 +0100
@@ -35,13 +35,17 @@
 
 fun is_tvar (x, _) = String.isPrefix "'" x;
 
-fun error_var msg xi = error (msg ^ Term.string_of_vname xi);
+fun error_var msg xi = error (msg ^ quote (Term.string_of_vname xi));
 
-fun the_sort tvars xi = the (AList.lookup (op =) tvars xi)
-  handle Option.Option => error_var "No such type variable in theorem: " xi;
+fun the_sort tvars (xi: indexname) =
+  (case AList.lookup (op =) tvars xi of
+    SOME S => S
+  | NONE => error_var "No such type variable in theorem: " xi);
 
-fun the_type vars xi = the (AList.lookup (op =) vars xi)
-  handle Option.Option => error_var "No such variable in theorem: " xi;
+fun the_type vars (xi: indexname) =
+  (case AList.lookup (op =) vars xi of
+    SOME T => T
+  | NONE => error_var "No such variable in theorem: " xi);
 
 fun unify_vartypes thy vars (xi, u) (unifier, maxidx) =
   let