src/HOL/Tools/record.ML
changeset 32765 3032c0308019
parent 32764 690f9cccf232
child 32767 2885e2a09f72
--- a/src/HOL/Tools/record.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/HOL/Tools/record.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -1732,7 +1732,7 @@
 
     (*before doing anything else, create the tree of new types
       that will back the record extension*)
-    (* FIXME cf. BalancedTree.make *)
+    (* FIXME cf. Balanced_Tree.make *)
     fun mktreeT [] = raise TYPE ("mktreeT: empty list", [], [])
       | mktreeT [T] = T
       | mktreeT xs =
@@ -1745,7 +1745,7 @@
             HOLogic.mk_prodT (mktreeT left, mktreeT right)
           end;
 
-    (* FIXME cf. BalancedTree.make *)
+    (* FIXME cf. Balanced_Tree.make *)
     fun mktreeV [] = raise TYPE ("mktreeV: empty list", [], [])
       | mktreeV [T] = T
       | mktreeV xs =