src/HOL/Nominal/nominal_primrec.ML
changeset 24867 e5b55d7be9bb
parent 24712 64ed05609568
child 24906 557a9cd9370c
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -416,6 +416,8 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 +val _ = OuterSyntax.keywords ["invariant", "freshness_context"];
     1.8 +
     1.9  val parser1 = P.$$$ "freshness_context" |-- P.$$$ ":" |-- (P.term >> SOME);
    1.10  val parser2 =
    1.11    P.$$$ "invariant" |-- P.$$$ ":" |--
    1.12 @@ -434,16 +436,13 @@
    1.13  val primrec_decl =
    1.14    options -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
    1.15  
    1.16 -val primrecP =
    1.17 +val _ =
    1.18    OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
    1.19      (primrec_decl >> (fn ((unchecked, (alt_name, (invs, fctxt))), eqns) =>
    1.20        Toplevel.print o Toplevel.theory_to_proof
    1.21          ((if unchecked then add_primrec_unchecked else add_primrec) alt_name invs fctxt
    1.22            (map P.triple_swap eqns))));
    1.23  
    1.24 -val _ = OuterSyntax.add_parsers [primrecP];
    1.25 -val _ = OuterSyntax.add_keywords ["invariant", "freshness_context"];
    1.26 -
    1.27  end;
    1.28  
    1.29