--- a/src/HOL/Tools/inductive_realizer.ML Wed Apr 13 18:45:25 2005 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Wed Apr 13 18:45:38 2005 +0200 @@ -480,3 +480,4 @@ "add realizers for inductive set")]]; end; +