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