src/HOLCF/Tools/fixrec.ML
changeset 33666 e49bfeb0d822
parent 33522 737589bb9bb8
child 33670 02b7738aef6a
equal deleted inserted replaced
33665:bdcabcffaaf6 33666:e49bfeb0d822
   240         val src = Attrib.internal (K add_unfold);
   240         val src = Attrib.internal (K add_unfold);
   241       in
   241       in
   242         ((thm_name, [src]), [thm])
   242         ((thm_name, [src]), [thm])
   243       end;
   243       end;
   244     val (thmss, lthy'') = lthy'
   244     val (thmss, lthy'') = lthy'
   245       |> fold_map (LocalTheory.note Thm.generatedK)
   245       |> fold_map (LocalTheory.note "") (induct_note :: map unfold_note unfold_thms);
   246         (induct_note :: map unfold_note unfold_thms);
       
   247   in
   246   in
   248     (lthy'', names, fixdef_thms, map snd unfold_thms)
   247     (lthy'', names, fixdef_thms, map snd unfold_thms)
   249   end;
   248   end;
   250 
   249 
   251 (*************************************************************************)
   250 (*************************************************************************)
   463       val simps1 : (Attrib.binding * thm list) list =
   462       val simps1 : (Attrib.binding * thm list) list =
   464         map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
   463         map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
   465       val simps2 : (Attrib.binding * thm list) list =
   464       val simps2 : (Attrib.binding * thm list) list =
   466         map (apsnd (fn thm => [thm])) (flat simps);
   465         map (apsnd (fn thm => [thm])) (flat simps);
   467       val (_, lthy'') = lthy'
   466       val (_, lthy'') = lthy'
   468         |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2);
   467         |> fold_map (LocalTheory.note "") (simps1 @ simps2);
   469     in
   468     in
   470       lthy''
   469       lthy''
   471     end
   470     end
   472     else lthy'
   471     else lthy'
   473   end;
   472   end;