# HG changeset patch
# User wenzelm
# Date 1392288854 -3600
# Node ID aa41ecbdc20520d77b77c4ef564aaba09b6cfdad
# Parent  e77f2858bd59c440ccb144df20efc3a041211b09
do not redefine outer syntax commands;

diff -r e77f2858bd59 -r aa41ecbdc205 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Thu Feb 13 11:37:00 2014 +0100
+++ b/etc/isar-keywords.el	Thu Feb 13 11:54:14 2014 +0100
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from HOL + HOL-Auth + HOL-BNF_Examples + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
+;; Generated from HOL + HOL-Auth + HOL-BNF_Examples + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Predicate_Compile_Examples + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
@@ -296,6 +296,7 @@
     "using"
     "value"
     "values"
+    "values_prolog"
     "welcome"
     "with"
     "wrap_free_constructors"
@@ -456,6 +457,7 @@
     "unused_thms"
     "value"
     "values"
+    "values_prolog"
     "welcome"))
 
 (defconst isar-keywords-theory-begin
diff -r e77f2858bd59 -r aa41ecbdc205 src/HOL/Library/Code_Prolog.thy
--- a/src/HOL/Library/Code_Prolog.thy	Thu Feb 13 11:37:00 2014 +0100
+++ b/src/HOL/Library/Code_Prolog.thy	Thu Feb 13 11:54:14 2014 +0100
@@ -6,6 +6,7 @@
 
 theory Code_Prolog
 imports Main
+keywords "values_prolog" :: diag
 begin
 
 ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
diff -r e77f2858bd59 -r aa41ecbdc205 src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Feb 13 11:37:00 2014 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Feb 13 11:54:14 2014 +0100
@@ -18,11 +18,11 @@
    replacing = [],
    manual_reorder = []}) *}
 
-values "{(x, y, z). append x y z}"
+values_prolog "{(x, y, z). append x y z}"
 
-values 4 "{(z, x, y). append x y ((1::nat) # (2 # (3 # z)))}"
+values_prolog 4 "{(z, x, y). append x y ((1::nat) # (2 # (3 # z)))}"
 
-values 3 "{(x, y, z). append x y z}"
+values_prolog 3 "{(x, y, z). append x y z}"
 
 setup {* Code_Prolog.map_code_options (K
   {ensure_groundness = false,
@@ -32,7 +32,7 @@
    replacing = [],
    manual_reorder = []}) *}
 
-values "{(x, y, z). append x y z}"
+values_prolog "{(x, y, z). append x y z}"
 
 setup {* Code_Prolog.map_code_options (K
   {ensure_groundness = false,
@@ -100,7 +100,7 @@
 where
   "queen [1,2,3,4,5,6,7,8,9] ys ==> queen_9 ys"
 
-values 10 "{ys. queen_9 ys}"
+values_prolog 10 "{ys. queen_9 ys}"
 
 
 section {* Example symbolic derivation *}
@@ -190,10 +190,10 @@
 where
   "d (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult x x) x) x) x) x) x) x) x) x) x e ==> times10 e"
 
-values "{e. ops8 e}"
-values "{e. divide10 e}"
-values "{e. log10 e}"
-values "{e. times10 e}"
+values_prolog "{e. ops8 e}"
+values_prolog "{e. divide10 e}"
+values_prolog "{e. log10 e}"
+values_prolog "{e. times10 e}"
 
 section {* Example negation *}
 
@@ -211,13 +211,13 @@
    replacing = [],
    manual_reorder = []}) *}
 
-values 2 "{y. notB y}"
+values_prolog 2 "{y. notB y}"
 
 inductive notAB :: "abc * abc \<Rightarrow> bool"
 where
   "y \<noteq> A \<Longrightarrow> z \<noteq> B \<Longrightarrow> notAB (y, z)"
 
-values 5 "{y. notAB y}"
+values_prolog 5 "{y. notAB y}"
 
 section {* Example prolog conform variable names *}
 
@@ -225,6 +225,6 @@
 where
   "equals y' y'"
 
-values 1 "{(y, z). equals y z}"
+values_prolog 1 "{(y, z). equals y z}"
 
 end
diff -r e77f2858bd59 -r aa41ecbdc205 src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Thu Feb 13 11:37:00 2014 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Thu Feb 13 11:54:14 2014 +0100
@@ -79,7 +79,7 @@
   replacing = [],
   manual_reorder = []}) *}
 
-values 40 "{s. hotel s}"
+values_prolog 40 "{s. hotel s}"
 
 setup {*
   Context.theory_map
diff -r e77f2858bd59 -r aa41ecbdc205 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Feb 13 11:37:00 2014 +0100
+++ b/src/HOL/ROOT	Thu Feb 13 11:54:14 2014 +0100
@@ -39,7 +39,7 @@
     AList_Mapping
     Code_Binary_Nat
     Code_Char
-    (* Code_Prolog  FIXME cf. 76965c356d2a *)
+    Code_Prolog
     Code_Real_Approx_By_Float
     Code_Target_Numeral
     DAList
diff -r e77f2858bd59 -r aa41ecbdc205 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Feb 13 11:37:00 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Feb 13 11:54:14 2014 +0100
@@ -1042,17 +1042,16 @@
   end |> Pretty.writeln
 
 
-(* renewing the values command for Prolog queries *)
+(* values command for Prolog queries *)
 
 val opt_print_modes =
   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "values"}
+  Outer_Syntax.improper_command @{command_spec "values_prolog"}
     "enumerate and print comprehensions"
     (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
-     >> (fn ((print_modes, soln), t) => Toplevel.keep
-          (values_cmd print_modes soln t))) (*FIXME does not preserve the previous functionality*)
+     >> (fn ((print_modes, soln), t) => Toplevel.keep (values_cmd print_modes soln t)))
 
 
 (* quickcheck generator *)