src/HOL/Tools/inductive_package.ML
changeset 17010 5abc26872268
parent 16975 34ed8d5d4f16
child 17057 0934ac31985f
--- a/src/HOL/Tools/inductive_package.ML	Wed Aug 03 14:48:13 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Wed Aug 03 14:48:22 2005 +0200
@@ -65,8 +65,8 @@
 (** theory context references **)
 
 val mono_name = "Orderings.mono";
-val gfp_name = "Gfp.gfp";
-val lfp_name = "Lfp.lfp";
+val gfp_name = "FixedPoint.gfp";
+val lfp_name = "FixedPoint.lfp";
 val vimage_name = "Set.vimage";
 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);