src/HOL/Tools/datatype_prop.ML
changeset 10911 eb5721204b38
parent 10214 77349ed89f45
child 11539 0f17da240450
--- a/src/HOL/Tools/datatype_prop.ML	Tue Jan 16 00:32:38 2001 +0100
+++ b/src/HOL/Tools/datatype_prop.ML	Tue Jan 16 00:33:40 2001 +0100
@@ -113,8 +113,9 @@
         fun mk_prem ((DtRec k, s), T) = HOLogic.mk_Trueprop
               (make_pred k T $ Free (s, T))
           | mk_prem ((DtType ("fun", [_, DtRec k]), s), T' as Type ("fun", [T, U])) =
-              HOLogic.mk_Trueprop (HOLogic.all_const T $
-                Abs ("x", T, make_pred k U $ (Free (s, T') $ Bound 0)));
+              (Const (InductivePackage.inductive_forall_name,
+                  [T --> HOLogic.boolT] ---> HOLogic.boolT) $
+                Abs ("x", T, make_pred k U $ (Free (s, T') $ Bound 0))) |> HOLogic.mk_Trueprop;
 
         val recs = filter is_rec_type cargs;
         val Ts = map (typ_of_dtyp descr' sorts) cargs;