# HG changeset patch
# User wenzelm
# Date 978899685 -3600
# Node ID 2ccc84b8f5a01a011308606c83013a93e51884df
# Parent  d466b42ad7a940383672ddc6ab958cb96fd36130
case binds: AutoBind.drop_judgment;

diff -r d466b42ad7a9 -r 2ccc84b8f5a0 src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Sun Jan 07 21:34:16 2001 +0100
+++ b/src/HOL/Tools/induct_method.ML	Sun Jan 07 21:34:45 2001 +0100
@@ -219,7 +219,8 @@
   let
     val ruly = Thm.term_of o rulify_cterm o cert;
     fun ruly_case {fixes, assumes, binds} =
-      {fixes = fixes, assumes = map ruly assumes, binds = map (apsnd (apsome ruly)) binds};
+      {fixes = fixes, assumes = map ruly assumes,
+        binds = map (apsnd (apsome (AutoBind.drop_judgment o ruly))) binds};
   in map (apsnd ruly_case) ooo RuleCases.make end;
 
 val weak_strip_tac = REPEAT o Tactic.match_tac [impI, allI, ballI];