--- a/src/HOL/Library/ROOT.ML Wed Aug 18 09:46:59 2010 +0200
+++ b/src/HOL/Library/ROOT.ML Wed Aug 18 09:46:59 2010 +0200
@@ -2,4 +2,4 @@
(* Classical Higher-order Logic -- batteries included *)
use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
- "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set", "Code_Prolog"];
+ "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)];
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Aug 18 09:46:59 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Aug 18 09:46:59 2010 +0200
@@ -414,6 +414,6 @@
val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
(opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
>> (fn ((print_modes, soln), t) => Toplevel.keep
- (values_cmd print_modes soln t)));
+ (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
end;