src/HOL/Nominal/nominal_primrec.ML
changeset 22101 6d13239d5f52
parent 21767 78ed5e22766a
child 22330 00ca68f5ce29
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri Jan 19 22:08:07 2007 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Jan 19 22:08:08 2007 +0100
     1.3 @@ -426,7 +426,7 @@
     1.4      (parser4 --| P.$$$ ")")) (false, ("", (NONE, NONE)));
     1.5  
     1.6  val primrec_decl =
     1.7 -  options -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
     1.8 +  options -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
     1.9  
    1.10  val primrecP =
    1.11    OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal