src/Pure/Isar/proof_context.ML

--- a/src/Pure/Isar/proof_context.ML	Fri Jul 01 22:35:20 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Jul 01 22:35:41 2005 +0200
@@ -1220,7 +1220,7 @@
     else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt)
   end;
 
-fun rem_case name = remove (fn (x, (y, _)) => x = y) name;
+fun rem_case name = remove (fn (x: string, (y, _)) => x = y) name;
 
 fun add_case ("", _) cases = cases
   | add_case (name, NONE) cases = rem_case name cases