# HG changeset patch # User haftmann # Date 1222186305 -7200 # Node ID e58ec46d50bcebc3c32c8e0218b8ecc4e0f03d44 # Parent 93964076e7b8a65cdd12df0a821909a91b7fbbcc fixed outer syntax diff -r 93964076e7b8 -r e58ec46d50bc src/Tools/code/code_funcgr.ML --- a/src/Tools/code/code_funcgr.ML Tue Sep 23 18:11:44 2008 +0200 +++ b/src/Tools/code/code_funcgr.ML Tue Sep 23 18:11:45 2008 +0200 @@ -316,13 +316,13 @@ val _ = OuterSyntax.improper_command "code_thms" "print system of defining equations for code" OuterKeyword.diag - (Scan.repeat P.term + (Scan.repeat P.term_group >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of))); val _ = OuterSyntax.improper_command "code_deps" "visualize dependencies of defining equations for code" OuterKeyword.diag - (Scan.repeat P.term + (Scan.repeat P.term_group >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));