# HG changeset patch
# User haftmann
# Date 1282117619 -7200
# Node ID 76965c356d2aed872e3a2af999adf666dcab61b8
# Parent  7115853eaf8a29f5962de95c3bfd7160e709e74c
removed Code_Prolog: modifies global environment setup non-conservatively

diff -r 7115853eaf8a -r 76965c356d2a src/HOL/Library/ROOT.ML
--- 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"*)];
diff -r 7115853eaf8a -r 76965c356d2a src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- 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;