1.1 --- a/src/HOL/Library/Eval.thy	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOL/Library/Eval.thy	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -213,14 +213,11 @@
     1.4  *}
     1.5  
     1.6  ML {*
     1.7 -val valueP =
     1.8    OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
     1.9      (Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")")
    1.10      -- OuterParse.term
    1.11        >> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep
    1.12             (Eval.evaluate_cmd some_name t)));
    1.13 -
    1.14 -val _ = OuterSyntax.add_parsers [valueP];
    1.15  *}
    1.16  
    1.17  end