# HG changeset patch
# User wenzelm
# Date 1137444917 -3600
# Node ID f3bfe81b6e58fefaa8b4a15c384b330b1424decf
# Parent  a95c2adc89006657c0c3d6811dd7b91137179563
case_result: drop_schematic, i.e. be permissive about illegal binds;

diff -r a95c2adc8900 -r f3bfe81b6e58 src/Pure/Isar/proof_context.ML
--- 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;