src/HOL/Tools/Predicate_Compile/code_prolog.ML
changeset 59936 b8ffc3dc9e24
parent 59582 0fbed69ff081
child 61268 abe08fb15a12
equal deleted inserted replaced
59935:343905de27b1 59936:b8ffc3dc9e24
  1031 
  1031 
  1032 val opt_print_modes =
  1032 val opt_print_modes =
  1033   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
  1033   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
  1034 
  1034 
  1035 val _ =
  1035 val _ =
  1036   Outer_Syntax.command @{command_spec "values_prolog"}
  1036   Outer_Syntax.command @{command_keyword values_prolog}
  1037     "enumerate and print comprehensions"
  1037     "enumerate and print comprehensions"
  1038     (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
  1038     (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
  1039      >> (fn ((print_modes, soln), t) => Toplevel.keep (values_cmd print_modes soln t)))
  1039      >> (fn ((print_modes, soln), t) => Toplevel.keep (values_cmd print_modes soln t)))
  1040 
  1040 
  1041 
  1041