# HG changeset patch
# User berghofe
# Date 1035212445 -7200
# Node ID c1637d60a846b3f81a51471550a984a655b018dd
# Parent  58bb243dbafbffe769f6f1f931eacd5ff0a52407
Now applies standard' to "unfold" theorem (due to flex-flex constraints).

diff -r 58bb243dbafb -r c1637d60a846 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Mon Oct 21 16:57:39 2002 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Mon Oct 21 17:00:45 2002 +0200
@@ -491,7 +491,7 @@
   let
     val _ = clean_message "  Proving the introduction rules ...";
 
-    val unfold = standard (mono RS (fp_def RS
+    val unfold = standard' (mono RS (fp_def RS
       (if coind then def_gfp_unfold else def_lfp_unfold)));
 
     fun select_disj 1 1 = []