# HG changeset patch
# User wenzelm
# Date 978899860 -3600
# Node ID 4e056473ae304d563e7002034f431b9c28bb075c
# Parent  37fa05a12459b796c412f66930923a3771c549c9
do not AutoBind.drop_judgment;

diff -r 37fa05a12459 -r 4e056473ae30 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Sun Jan 07 21:36:59 2001 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Sun Jan 07 21:37:40 2001 +0100
@@ -84,7 +84,7 @@
       |> map (if open_parms then I else apfst Syntax.internal);
     val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi);
     val concl_bind = ((case_conclN, 0),
-      Some (Term.list_abs (xs, AutoBind.drop_judgment (Logic.strip_assums_concl Bi))));
+      Some (Term.list_abs (xs, Logic.strip_assums_concl Bi)));
   in (name, {fixes = xs, assumes = asms, binds = [concl_bind]}) end;
 
 fun make open_parms raw_thm names =