src/HOL/Tools/old_primrec.ML
changeset 32863 5e8cef567042
parent 32727 9072201cd69d
child 33037 b22e44496dc2
equal deleted inserted replaced
32862:1fc86cec3bdf 32863:5e8cef567042
   316 
   316 
   317 val add_primrec = gen_primrec thy_note (thy_def false);
   317 val add_primrec = gen_primrec thy_note (thy_def false);
   318 val add_primrec_unchecked = gen_primrec thy_note (thy_def true);
   318 val add_primrec_unchecked = gen_primrec thy_note (thy_def true);
   319 val add_primrec_i = gen_primrec_i thy_note (thy_def false);
   319 val add_primrec_i = gen_primrec_i thy_note (thy_def false);
   320 val add_primrec_unchecked_i = gen_primrec_i thy_note (thy_def true);
   320 val add_primrec_unchecked_i = gen_primrec_i thy_note (thy_def true);
   321 fun gen_primrec note def alt_name specs =
       
   322   gen_primrec_i note def alt_name (map (fn ((name, t), atts) => ((name, atts), t)) specs);
       
   323 
   321 
   324 end;
   322 end;
   325 
   323 
   326 
       
   327 (* see primrec.ML (* outer syntax *)
       
   328 
       
   329 local structure P = OuterParse and K = OuterKeyword in
       
   330 
       
   331 val opt_unchecked_name =
       
   332   Scan.optional (P.$$$ "(" |-- P.!!!
       
   333     (((P.$$$ "unchecked" >> K true) -- Scan.optional P.name "" ||
       
   334       P.name >> pair false) --| P.$$$ ")")) (false, "");
       
   335 
       
   336 val primrec_decl =
       
   337   opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
       
   338 
       
   339 val _ =
       
   340   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
       
   341     (primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
       
   342       Toplevel.theory (snd o
       
   343         (if unchecked then add_primrec_unchecked else add_primrec) alt_name
       
   344           (map P.triple_swap eqns))));
       
   345 
       
   346 end;*)
       
   347 
       
   348 end;
   324 end;