induct cases: RuleCases.make_raw;
authorwenzelm
Thu Jan 11 19:38:02 2001 +0100 (2001-01-11)
changeset 108710ff9caa810b1
parent 10870 9444e3cf37e1
child 10872 87bb4462c434
induct cases: RuleCases.make_raw;
src/HOL/Tools/induct_method.ML
     1.1 --- a/src/HOL/Tools/induct_method.ML	Thu Jan 11 19:37:46 2001 +0100
     1.2 +++ b/src/HOL/Tools/induct_method.ML	Thu Jan 11 19:38:02 2001 +0100
     1.3 @@ -221,7 +221,7 @@
     1.4      fun ruly_case {fixes, assumes, binds} =
     1.5        {fixes = fixes, assumes = map ruly assumes,
     1.6          binds = map (apsnd (apsome (AutoBind.drop_judgment o ruly))) binds};
     1.7 -  in map (apsnd ruly_case) ooo RuleCases.make end;
     1.8 +  in map (apsnd ruly_case) ooo RuleCases.make_raw end;
     1.9  
    1.10  val weak_strip_tac = REPEAT o Tactic.match_tac [impI, allI, ballI];
    1.11