src/HOL/Tools/old_primrec.ML
changeset 33317 b4534348b8fd
parent 33056 791a4655cae3
child 33338 de76079f973a
equal deleted inserted replaced
33316:6a72af4e84b8 33317:b4534348b8fd
   193 fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) =
   193 fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) =
   194   case AList.lookup (op =) fns i of
   194   case AList.lookup (op =) fns i of
   195      NONE =>
   195      NONE =>
   196        let
   196        let
   197          val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined",
   197          val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined",
   198            replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
   198            replicate (length cargs + length (filter is_rec_type cargs))
   199              dummyT ---> HOLogic.unitT)) constrs;
   199              dummyT ---> HOLogic.unitT)) constrs;
   200          val _ = warning ("No function definition for datatype " ^ quote tname)
   200          val _ = warning ("No function definition for datatype " ^ quote tname)
   201        in
   201        in
   202          (dummy_fns @ fs, defs)
   202          (dummy_fns @ fs, defs)
   203        end
   203        end