src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
changeset 56945 3d1ead21a055
parent 56858 0c3d0bc98abe
child 57303 498a62e65f5f
equal deleted inserted replaced
56944:578dc6b4be89 56945:3d1ead21a055
  1429     fun after_qed thmss' = fold_map Local_Theory.define defs #-> prove thmss';
  1429     fun after_qed thmss' = fold_map Local_Theory.define defs #-> prove thmss';
  1430   in
  1430   in
  1431     (goalss, after_qed, lthy')
  1431     (goalss, after_qed, lthy')
  1432   end;
  1432   end;
  1433 
  1433 
  1434 fun add_primcorec_ursive_cmd auto opts (raw_fixes, raw_specs') lthy =
  1434 fun add_primcorec_ursive_cmd auto opts (raw_fixes, raw_specs_of) lthy =
  1435   let
  1435   let
  1436     val (raw_specs, of_specs_opt) =
  1436     val (raw_specs, of_specs_opt) =
  1437       split_list raw_specs' ||> map (Option.map (Syntax.read_term lthy));
  1437       split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy));
  1438     val ((fixes, specs), _) = Specification.read_spec raw_fixes raw_specs lthy;
  1438     val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy);
  1439   in
  1439   in
  1440     add_primcorec_ursive auto opts fixes specs of_specs_opt lthy
  1440     add_primcorec_ursive auto opts fixes specs of_specs_opt lthy
  1441     handle ERROR str => primcorec_error str
  1441     handle ERROR str => primcorec_error str
  1442   end
  1442   end
  1443   handle PRIMCOREC (str, eqns) =>
  1443   handle PRIMCOREC (str, eqns) =>