# HG changeset patch
# User wenzelm
# Date 979238282 -3600
# Node ID 0ff9caa810b10fb524f891eaf9abf01495872b5d
# Parent  9444e3cf37e11e5bffabe2996e6fd0e80d203d4d
induct cases: RuleCases.make_raw;

diff -r 9444e3cf37e1 -r 0ff9caa810b1 src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Thu Jan 11 19:37:46 2001 +0100
+++ b/src/HOL/Tools/induct_method.ML	Thu Jan 11 19:38:02 2001 +0100
@@ -221,7 +221,7 @@
     fun ruly_case {fixes, assumes, 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;
+  in map (apsnd ruly_case) ooo RuleCases.make_raw end;
 
 val weak_strip_tac = REPEAT o Tactic.match_tac [impI, allI, ballI];