src/HOL/Tools/old_primrec.ML
changeset 32863 5e8cef567042
parent 32727 9072201cd69d
child 33037 b22e44496dc2
     1.1 --- a/src/HOL/Tools/old_primrec.ML	Fri Oct 02 22:15:30 2009 +0200
     1.2 +++ b/src/HOL/Tools/old_primrec.ML	Fri Oct 02 23:15:36 2009 +0200
     1.3 @@ -318,31 +318,7 @@
     1.4  val add_primrec_unchecked = gen_primrec thy_note (thy_def true);
     1.5  val add_primrec_i = gen_primrec_i thy_note (thy_def false);
     1.6  val add_primrec_unchecked_i = gen_primrec_i thy_note (thy_def true);
     1.7 -fun gen_primrec note def alt_name specs =
     1.8 -  gen_primrec_i note def alt_name (map (fn ((name, t), atts) => ((name, atts), t)) specs);
     1.9  
    1.10  end;
    1.11  
    1.12 -
    1.13 -(* see primrec.ML (* outer syntax *)
    1.14 -
    1.15 -local structure P = OuterParse and K = OuterKeyword in
    1.16 -
    1.17 -val opt_unchecked_name =
    1.18 -  Scan.optional (P.$$$ "(" |-- P.!!!
    1.19 -    (((P.$$$ "unchecked" >> K true) -- Scan.optional P.name "" ||
    1.20 -      P.name >> pair false) --| P.$$$ ")")) (false, "");
    1.21 -
    1.22 -val primrec_decl =
    1.23 -  opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
    1.24 -
    1.25 -val _ =
    1.26 -  OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
    1.27 -    (primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
    1.28 -      Toplevel.theory (snd o
    1.29 -        (if unchecked then add_primrec_unchecked else add_primrec) alt_name
    1.30 -          (map P.triple_swap eqns))));
    1.31 -
    1.32 -end;*)
    1.33 -
    1.34  end;