src/HOL/Tools/inductive_package.ML
changeset 13657 c1637d60a846
parent 13626 282fbabec862
child 13709 ec00ba43aee8
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Oct 21 16:57:39 2002 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Oct 21 17:00:45 2002 +0200
     1.3 @@ -491,7 +491,7 @@
     1.4    let
     1.5      val _ = clean_message "  Proving the introduction rules ...";
     1.6  
     1.7 -    val unfold = standard (mono RS (fp_def RS
     1.8 +    val unfold = standard' (mono RS (fp_def RS
     1.9        (if coind then def_gfp_unfold else def_lfp_unfold)));
    1.10  
    1.11      fun select_disj 1 1 = []