changeset 18699 | f3bfe81b6e58 |
parent 18678 | dd0c569fa43d |
child 18708 | 4b3dadb4fe33 |
--- 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;