src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 33519 e31a85f92ce9
parent 33487 6fe8b9baf4db
child 33522 737589bb9bb8
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -2450,7 +2450,7 @@
   (*FIXME name discrepancy in attribs and ML code*)
   (*FIXME intros should be better named intro*)
 
-(* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
+(* TODO: make TheoryDataFun to Generic_Data & remove duplication of local theory and theory *)
 fun generic_code_pred prep_const options raw_const lthy =
   let
     val thy = ProofContext.theory_of lthy