# HG changeset patch # User wenzelm # Date 1113410738 -7200 # Node ID bc264e730103f8b775b2b7c2f202b93a17635e89 # Parent b5edb9dcec9ad1b09812cc846db4fc75099314bc *** MESSAGE REFERS TO PREVIOUS VERSION *** Args.global_const (static binding!); diff -r b5edb9dcec9a -r bc264e730103 src/HOL/Tools/inductive_realizer.ML --- 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; +