src/HOL/Tools/recfun_codegen.ML
changeset 30190 479806475f3c
parent 29272 fb3ccf499df5
child 31036 64ff53fc0c0c
equal deleted inserted replaced
30189:3633f560f4c3 30190:479806475f3c
   141                  val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
   141                  val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
   142                  val module' = if_library thyname module;
   142                  val module' = if_library thyname module;
   143                  val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
   143                  val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
   144                  val (fundef', gr3) = mk_fundef module' "" true eqs''
   144                  val (fundef', gr3) = mk_fundef module' "" true eqs''
   145                    (add_edge (dname, dep)
   145                    (add_edge (dname, dep)
   146                      (foldr (uncurry new_node) (del_nodes xs gr2)
   146                      (List.foldr (uncurry new_node) (del_nodes xs gr2)
   147                        (map (fn k =>
   147                        (map (fn k =>
   148                          (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs)))
   148                          (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs)))
   149                in (module', put_code module' fundef' gr3) end
   149                in (module', put_code module' fundef' gr3) end
   150              else (module, gr2))
   150              else (module, gr2))
   151          end
   151          end