case_result: drop_schematic, i.e. be permissive about illegal binds;

--- a/src/Pure/Isar/proof_context.ML	Mon Jan 16 21:55:15 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Jan 16 21:55:17 2006 +0100
@@ -1308,7 +1308,7 @@
     val RuleCases.Case {assumes, binds, cases, ...} = RuleCases.apply ts c;
   in
     ctxt'
-    |> add_binds_i binds
+    |> add_binds_i (map drop_schematic binds)
     |> add_cases true (map (apsnd SOME) cases)
     |> pair (assumes, (binds, cases))
   end;