# 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;
+